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.
New: use Timbuk for verifying HigherOrder Functional Programs ... For instance, Timbuk is used to verify HigherOrder Functional Programs, Java programs and Cryptographic Protocols (see some papers...

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 ...

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...