Tools on Rewriting

Timbuk is a collection of tools for achieving proofs of reachability over Term Rewriting Systems and for manipulating Tree Automata (bottomup nondeterministic finite tree automata). Timbuk and reachability analysis can be used for program verification.
[GGHL18] (pdf) T. Genet, T. Gillard, T. Haudebourg, S. Lê Cong. Extending Timbuk to Verify Functional Programs. In Proceedings of WRLA'18, To be published. SpringerVerlag, ...

Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program. Agda is a proof assistant. It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory.
Page last modified on April 11, 2018, at 09:48 AM...

The SToUT (Symbolic Computation Techniques for Unranked Terms) project provides a library for unification and antiunification algorithms: unification with sequence variables, context sequence matching, rigid antiunification for unranked terms and hedges, unranked secondorder antiunification, higherorder antiunification, nominal antiunification.
Information and Computation. 255, part 2. 262286, 2017. PDF, BibTeX. ... Reasoning. 58(2):293310, 2017....

A Coq library on rewriting and termination with tactics for automatically checking the conditions of termination theorems.
theorems on rewriting theory, lcalculus and termination whose correctness has been mechanically checked by the Coq proof assistant. See this paper for some presentation. More papers are provided ...

Q is an interpreted, dynamically typed functional programming language based on term rewriting which allows you to define functions using symbolic equations. It works on Linux, OS X, Unix and Windows, and comes with a bunch of useful libraries which turn it into a practical programming tool. The Q programming system is free software distributed under the GPL.
Q  Equational Programming Language ... News About Examples Documentation Lists Core AddOns Download Links [SourceForge] ... Please note that Q has been superseded by the Pure progr...

Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixedsize bitvectors, quantifiers, and lambda expressions. Yices also does MaxSMT (and, dually, unsat cores) and is competitive as an ordinary SAT and MaxSAT solver.
* Report a Bug...

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.
Last updated: 20171230 16:57:08...

ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semiautomatic theorem prover, just to name its most common uses.
ACL2 Version 8.0 ... [note02.gif] Differences from Version 7.4 [twarning.gif] [file04.gif] ... December 12, 2017 ... * ACL2+Books Manual (Version 8.0) ... * ACL2 User's Manual (Version 8.0)...

The Nagoya Termination Tool (NaTT) is a termination prover for term rewrite systems (TRSs), which is special for: its power due to the implementation of the weighted path order (WPO), its efficiency due to the strong cooperation with external SMT solvers, and use of the DP framework for proving relative termination
The Nagoya Termination Tool (NaTT) ... NaTT [YKS14] is a termination prover for term rewrite systems (TRSs), which is special for: * its power due to the implementation of the weighted path orde...

Objective Caml is the most popular variant of the Caml language. From a language standpoint, it extends the core Caml language with a fullyfledged objectoriented layer, as well as a powerful module system, all connected by a sound, polymorphic type system featuring type inference. The Objective Caml system is an industrialstrength implementation of this language, featuring a highperformance nativecode compiler (ocamlopt) for 9 processor architectures (IA32, PowerPC, AMD64, Alpha, Sparc, Mips, IA64, HPPA, StrongArm), as well as a bytecode compiler (ocamlc) and an interactive readevalprint loop (ocaml) for quick development and portability.

MINLOG is an interactive proof system developed by Helmut Schwichtenberg and members of the logic group at the University of Munich. MINLOG is based on first order natural deduction calculus. It is intended to reason about computable functionals, using minimal rather than classical or intuitionistic logic. The main motivation behind MINLOG is to exploit the proofsasprograms paradigm for program development and program verification. Proofs are in fact treated as first class objects which can be normalized. If a formula is existential then its proof can be used for reading off an instance of it, or changed appropriately for program development by proof transformation. To this end MINLOG is equipped with tools to extract functional programs directly from proof terms. This also applies to nonconstructive proofs, using a refined Atranslation. The system is supported by automatic proof search and normalization by evaluation as an efficient term rewriting device.
The case studies contain material from the following publications: ... Schwichtenberg and H. Tsuiki. (In D. Probst and P. Schuster (eds), Concepts of Proof in Mathematics, Philosophy, and Comput...

PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the stateoftheart in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. PVS is a research prototype: it evolves and improves as we develop or apply new capabilities, and as the stress of real use exposes new requirements.
Last modified: Wed 05 Feb 2014 23:49 UTC...

Maude is a highperformance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications. Maude has been influenced in important ways by the OBJ3 language, which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation.
* Bug Reports and Mailing Lists ... * This page was last modified on 18 September 2017, at 19:16. * This page has been accessed 200,766 times....

TRS.Tool is a teachingoriented tool that can be used to learn the basic notions and concepts of term rewriting. Accordingly, it gives a lot of explicit and intermediate information about signatures, terms, positions, rules, and term rewriting systems, and also about the analysis of critical pairs. We hope that this approach will be useful to get undergraduate students (and interested people) familiarized with the basic rewriting theory and then become involved in the field.

SML# is a new programming language in the Standard ML family being developed at RIEC (Research Institute of Electrical Communication), Tohoku University jointly with Sanpu Koubou Inc. Its design goal is to provide a moderate but practically important extensions (see features of SML#) while maintaining the compatibility of the Definition of Standard ML.
* Version 3.4.0 has been released. ... Last modified:2017/08/31 21:50:03 ... + SML# 3.4.0 has been released (Aug 31th, 2017)....

PρLog (pronounced Pērōlog) is an experimental tool that extends logic programming with strategic conditional transformation rules, combining Prolog with ρLog calculus. It deals with term sequences (also called hedges), transforming them by conditional rules. Transformations are nondeterministic and may yield several results. Strategies provide a control on rule applications in a declarative way. The rules apply matching to the whole input hedge (or, if it is a single term, apply at the top position). Four different types of variables (for terms, term sequences, function symbols, and contexts) give the user flexible control on selecting terms in hedges or subterms in terms. As a result, the obtained code is usually quite short and declaratively clear.

The Tyrolean Termination Tool 2 (TTT2) is a tool for automatically proving (and disproving) termination of rewrite systems. It is the completely redesigned successor of TTT. Current (non)termination techniques include approximated dependency graph, argument filtering, bounds, dependency pair method, KnuthBendix order, lexicographic path order, loop detection, matrix interpretation, polynomial interpretation, predictive labeling, recursive SCC, root labeling, semantic labeling, simple projection and subterm criterion, uncurrying, usable rules.
The current version is 1.16.2. Get recent versions. Or directly access...

μTerm is a tool which can be used to verify a number of termination properties of Term Rewriting Systems via different reduction relations which can be associated to them: termination of rewriting, termination of innermost rewriting, termination of contextsensitive rewriting, and termination of innermost contextsensitive rewriting.
Union Europea Â Â [2011WebEconomiaC63px.jpg] [logo_SEIDI.jpg]...

Stratego/XT is a language and toolset for program transformation. The Stratego language provides rewrite rules for expressing basic transformations, programmable rewriting strategies for controlling the application of rules, concrete syntax for expressing the patterns of rules in the syntax of the object language, and dynamic rewrite rules for expressing contextsensitive transformations, thus supporting the development of transformation components at a high level of abstraction.
website for information and downloads: http://metaborg.org. This website is still available for historical purposes. Refer the new site for uptodate documentation....

MiniSat is a minimalistic, opensource SAT solver, developed to help researchers and developers alike to get started on SAT. Some key features of MiniSat: * Easy to modify. MiniSat is small and welldocumented, and possibly also welldesigned, making it an ideal starting point for adapting SAT based techniques to domain specific problems. * Highly efficient. Winning all the industrial categories of the SAT 2005 competition, MiniSat is a good starting point both for future research in SAT, and for applications using SAT. * Designed for integration. MiniSat supports incremental SAT and has mechanisms for adding nonclausal constraints. By virtue of being easy to modify, it is a good choice for integrating as a backend to another tool, such as a model checker or a more generic constraint solver.

AProVE is a system for automated termination and innermost termination proofs of term rewrite systems (TRSs). Moreover, AProVE also handles several other formalisms, e.g., logic programs (Prolog), functional programs (Haskell 98), conditional TRSs, TRSs modulo AC, contextsensitive TRSs, etc. The power of AProVE is demonstrated in the annual International Competition of Termination Tools, where AProVE was the most powerful tool for termination of TRSs in 2004, 2005, 2006, 2007, and 2008.
(Java Bytecode and C / LLVM), functional programs (Haskell 98), and logic programs (Prolog). The power of AProVE is demonstrated in the annual International Competition of Termination Tools and In...

CafeOBJ is a new generation algebraic specification and programming language. As a direct successor of OBJ, it inherits all its features (flexible mixfix syntax, powerful typing system with subtypes, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the parameters, module expressions, etc.) but it also implements new paradigms such as rewriting logic and hidden algebra, as well as their combination.

The Tyrolean Complexity Tool (TCT) is a tool for automatically proving (low) upper bounds on the derivational complexity and runtime complexity of terminating term rewriting systems. Whereas Version 1.0 is strongly based on the automatic termination prover TTT2, Version 2.0 is rewritten from scratch in the purely functional programming language Haskell.
CBR Home TcT Home Download Experiments TCT Web...

REPIUS (REwriteProgram Inversion and Unraveling System) is a tool that (fully or partially) inverts a constructor TRS written in a .trs file and unravels the resulting inverse CTRS. The prototype (Ver. 0.x) was developed following the approach in (Nishida et al., RTA'05) and employs a variant of Ohlebusch's unraveling transformation. The current version was wholly implemented, introducing a new approach to tailrecursive functions into the previous approach to full inversion (Nishida et al., IEICE'05). The unraveling step will be implemented as an option of postprocess of inversion, and the partial inversion approach will be also implemented as an extension. The current implementation is based on the technique in (Nishida and Vidal, RTA'11).
Updated: Oct 21, 2015 ... repius.jar (Jun 27, 2012)...

Autowrite is a project carried out at the LaBRI (Laboratoire Bordelais de Recherche en Informatique) at the University of Bordeaux. Autowrite is an experimental tool written in Common Lisp for checking properties of term rewrite systems and handling bottomup term (tree) automata. It is written in Steele Bank Common Lisp (SBCL). It was initially designed to check callbyneed (CBN) properties of TRSs. For this purpose, it also implements the main operations on term automata constructions (determinization, minimization, union, intersection, emptiness, ...) and many operations on terms. Recently, flyautomata have been added to the implementation. The transition function of a flyautomaton is a (Lisp) transition function instead of a table of transitions. Flyautomata may be used when the transition table is too big to be stored and can also be infinite in two ways (infinite signature, infinite number of states). A graphical interface interface written using FreeCLIM, the free implementation of the CLIM specification frees the user from any Lisp knowledge. From this interface, one can handle term rewrite systems, term automata and build many term automata related to TRSs and graphs represented as terms; one can check membership to callbyneed classes for the different considered approximations of a given system.
is written in Steele Bank Common Lisp ( SBCL). It was initially designed to check callbyneed (CBN) properties of TRSs. For this purpose, it also implements the main operations on term automata ...

GURU is a pure functional programming language, which is similar in some ways to Caml and Haskell. But GURU also contains a language for writing formal proofs demonstrating the properties of programs. So there are really two languages: the language of programs, and the language of proofs. When the compiler checks a program, it computes a type for it, just as compilers for other languages like JAVA do. But in GURU, such types can be significantly richer than in mainstream or even most research programming languages. These types are called dependent types, and they can express nontrivial semantic properties of data and functions. Analogously, when the compiler checks a proof, it computes a formula for it, namely the formula the proof proves. So we really have four kinds of expressions in GURU: programs (which we also call terms) and their types; proofs and their formulas.
READONLY: This project has been archived. For more information see this post....

ACP is an automated confluence prover for term rewriting systems (TRSs). A distinct feature of ACP is incorporation of several divideandconquer criteria such as those for commutative (Toyama,1988), layerpreserving (Ohlebusch,1994) and persistent (Aoto and Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non)confluence of the whole system.
the whole system. ACP is participating Confluence Competition (CoCo). ... Support of certificates generation For few criteria, ACP can generate certificates in CPF format, w...

Saigawa is an automatic confluence tool for firstorder term rewrite systems. It supports the next confluence criteria: Knuth and Bendix' criterion, decreasing confluence, and rulelabeling
* CoLLSaigawa 1.0 released. This is a combination of CoLL 1.1 and Saigawa 1.8. This version participates in the 4th Confluence Competition (CoCo 2014) * CoLL 1.1 released. ... * CoLL...

Z3 is a highperformance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixedsize bitvectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. These include: Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, and HAVOC. It can read problems in SMTLIB and Simplify formats.
Z3: Theorem Prover ... See main wiki page. ... The API documentation is available here....

Autograph is a project carried out at the LaBRI (Laboratoire Bordelais de Recherche en Informatique) at the University of Bordeaux. Autograph is an experimental tool written in Common Lisp for verifying properties of graphs of bounded cliquewidth. It is written in Steele Bank Common Lisp (SBCL). It uses the Autowrite library which provides the operations needed to create and manipulate automata. The following famous theorem connects the problem of verifying graph properties with term automata: Monadic secondorder model checking is for treewidth [Courcelle (1990)] and cliquewidth [Courcelle, Makowski, Rotics (2001)]. Treewidth and cliquewidth are graph complexity measures based on graph decompositions. A decomposition produces a term representation of the graph. For a graph property expressed in monadic second order logic (MSO), the algorithm verifying the property takes the form of a term automaton which recognizes the terms denoting graphs satisfying the property.
Autograph is now part of TRAG ... git clone https://idurand@bitbucket.org/idurand/trag.git...

By this tool proofs of (relative) termination of string rewriting systems (SRS) can be generated automatically. It was developed by Hans Zantema starting in July 2003. It is based on a combination of polynomial and matrix interpretations, recursive path order, semantic labelling, dependency pairs, transformation order, dummy elimination and RFCmatchbounds. Proofs of nontermination are found by using ancestor graphs. In both the termination competition of 2004 and the termination competition of 2005 this tool performed the best of all tools in the category of string rewriting.

CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order theory (or a combination of such theories). It is the fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code from any previous version. CVC4 is intended to be an open and extensible SMT engine. It can be used as a standalone tool or as a library. It has been designed to increase the performance and reduce the memory overhead of its predecessors. CVC4 is still a research prototype and is not yet ready for public release. Users looking for an industrialstrength SMT solver are encouraged to use CVC3 instead (for now).
* Google...

GHC is a stateoftheart, open source, compiler and interactive environment for the functional language Haskell. Highlights: * GHC supports the entire Haskell 2010 language plus a wide variety of extensions. * GHC has particularly good support for concurrency and parallelism, including support for Software Transactional Memory (STM). * GHC generates fast code, particularly for concurrent programs. Take a look at GHC's performance on The Computer Language Benchmarks Game. * GHC works on several platforms including Windows, Mac, Linux, most varieties of Unix, and several different processor architectures. There are detailed instructions for porting GHC to a new platform. * GHC has extensive optimisation capabilities, including intermodule optimisation. * GHC compiles Haskell code either directly to native code or using LLVM as a backend. GHC can also generate C code as an intermediate target for porting to new platforms. The interactive environment compiles Haskell to bytecode, and supports execution of mixed bytecode/compiled programs. * Profiling is supported, both by time/allocation and various kinds of heap profiling. * GHC comes with several libraries, and thousands more are available on Hackage.
11 July 2014 GHC 7.8.3 Released! [download]...

MiniSmt is a simple SMT solver for nonlinear arithmetic based on MiniSat and Yices. It accepts the SMTLIB format as input, is efficient on small domains, supports reasoning about nonrational real numbers, and is able to output models.
The current stable version is 0.6. Get recent versions and view the ... Mar 9, 2014: version 0.6 released (compile with interfaced GPW)...

The CRSX project aims at implementing a generic higherorder rewrite engine based on the Combinatory Reduction Systems (CRS) formalism.
CRSXCombinatory Reduction Systems with Extensions. ... CRSX implements higherorder rewriting based on Combinatory Reduction Systems (CRS) with some extensions. ... Copyright (c) 2006, 2013 IBM Co...

CITP is a tool for proving inductive properties of software systems specified with constructor based logics. CITP is equipped with a default proof strategy for the automated verification of Observational Transitional Systems (OTS), but the area of applications is not restricted to OTS. The proof strategy can be customised by the user, or the basic tactics can be applied stepbystep. The Kernel of CITP is implemented in Core Maude. The interface of CITP is implemented in Full Maude.

The aim of the system daTac is to do automated deduction in firstorder logic with equality. Its speciality is to apply deductions modulo some equational properties of operators, such as commutativity or associativitycommutativity (AC). The deduction techniques implemented, based on resolution, paramodulation and term rewriting, have been proved refutationally complete.

CaT is a powerful analyzer for the complexity of term rewrite systems. It is based on the fast and powerful termination analyzer TTT2. In 2008 and 2009, CaT won all categories in the international termination competition related to complexity in which it participated.
2010, 2011, 2012, and 2013 in the international termination competition....

Soot is a Java optimization framework. It provides four intermediate representations for analyzing and transforming Java bytecode: 1. Baf: a streamlined representation of bytecode which is simple to manipulate. 2. Jimple: a typed 3address intermediate representation suitable for optimization. 3. Shimple: an SSA variation of Jimple. 4. Grimp: an aggregated version of Jimple suitable for decompilation and code inspection. Soot can be used as a stand alone tool to optimize or inspect class files, as well as a framework to develop optimizations or transformations on Java bytecode.
Unreleased versions can be found in the github repository....

iProver is an instantiationbased theorem prover which is based on InstGen calculus, complete for firstorder logic. One of the distinctive features of iProver is a modular combination of instantiation and propositional reasoning. In particular, any stateofthe art SAT solver can be integrated into our framework. iProver incorporates stateoftheart implementation techniques such as indexing, redundancy elimination, semantic selection and saturation algorithms. Redundancy elimination implemented in iProver include: dismatching constraints, blocking nonproper instantiations and propositionalbased simplifications. In addition to instantiation, iProver implements ordered resolution calculus and a combination of instantiation and ordered resolution.
New version: iProver v0.99 (CASCJ6, 2012) to be released in a few days!!! ... Easy to install: We assume OCaml v3.12 >= is installed. ... iProver won the (effectively propositional) EPR division...

QEPCAD is an implementation of quantifier elimination by partial cylindrical algebraic decomposition due originally to Hoon Hong, and subsequently added on to by many others. It is an interactive commandline program written in C, and based on the SACLIB library of computer algebra functions. Presented here is QEPCAD B version 1, the B designating a substantial departure from the original QEPCAD and distinguishing it from any development of the original that may proceed in a different direction.
The current version of QEPCADB is Version B 1.69, 16 March 2012....

E is a a purely equational theorem prover for full firstorder logic. That means it is a program that you can stuff a mathematical specification (in firstorder format) and a hypothesis into, and which will then run forever, using up all of your machines resources. Very occasionally it will find a proof for the hypothesis and tell you so...

CiME 3 is a rewriting toolbox that provides Coq certificates for termination proofs (standard rewriting) obtained using various criteria: Dependency pairs (plain/marks, graphs refinements with or without subterm criterion), as well as various orderings (polynomial interpretations, matrix interpretations, full RPO with status, with AFS refinements).

mkbTT is a tool for performing KnuthBendix completion with automatic termination tools. It is based on two ingredients: (1) the inference system for completion with multiple reduction orderings introduced by Kurihara and Kondo (1999) and (2) the inference system for completion with external termination provers proposed by Wehrman, Stump and Westbrook (2006). The tool can be used with any termination tool that satisfies certain minimal requirements.
Home Download Usage Web Interface Experiments...

RAPT (Rewritingbased Automated Program Transformation system) is a program transformation system using transformation templates, which implements a framework of program transformation. RAPT transforms manysorted TRSs according to input correct templates with verification of its correctness.
chiba...

Vienna Modular Termination Laboratory (VMTL) is a tool for the (semi)automatic termination analysis of rewriting systems. Currently, standard as well as contextsensitive and conditional term rewriting systems are supported. VMTL is an implementation of the dependency pair framework, in which termination of rewrite systems is analyzed by so called dependency pair processors. The search for termination proofs in VMTL is guided by a user configurable strategy featuring hierarchical grouping of processors, timelimits on the level of processor groups as well as single processors and parallelization. In addition VMTL provides open interfaces allowing to add new dependency pair processors as well as transformations/preprocessings of rewrite systems in a modular fashion.