for Reachability Analysis and
Tree Automata Calculations

What is Timbuk?

Timbuk is a collection of tools for achieving proofs of reachability over Term Rewriting Systems and for manipulating Tree Automata (bottom-up non-deterministic finite tree automata)

Timbuk and reachability analysis can be used for program verification. For instance, Timbuk is currently used to verify Cryptographic Protocols (see some papers and in the examples of the distribution).

Timbuk 3.0 is a fully new version of the tree automata completion engine used for reachability analysis. Older Timbuk distributions (2.2) provide three standalone tools and a bunch of Objective Caml functions for basic manipulation on Tree Automata, alphabets, terms, Term Rewriting Systems, etc. The three tools are:

Timbuk: a tree automata completion engine for reachability analysis over Term Rewriting Systems

Taml: an Ocaml toplevel with basic functions on tree automata:

boolean operations: intersection, union, inversion
emptyness decision, inclusion decision
cleaning, renaming
determinisation
matching of terms over tree automata
producing the automaton recognizing terms irreducible w.r.t. a Term Rewriting System
normalization of transitions
parsing, pretty printing
reading and writing automata to disk
and some more

Tabi: a Tree Automata Browsing Interface for visual automata inspection. This tool permits to build interactively and graphically some representatives of the language recognized by a tree automaton. Like this

Note that if you plan to use Tabi, you need a working Tcl/Tk library on your system (see README file for details)

Tree Automata Completion Checker is available! This checker certifies that a tree automaton, obtained by tree automata completion, recognizes a superset of reachable terms. It consists of Ocaml functions extracter from a Coq specification of tree automata completion. The principle is describe in the IJCAR paper that can be found here, the code can be downloaded here.

License

Timbuk 1.0 to 2.2 : Copyright (C) 2000-2003 Thomas Genet and Valérie Viet Triem Tong

Timbuk 3.0 : Copyright (C) 2009 Thomas Genet and Yohan Boichut

Taml: Copyright (C) 2003 Thomas Genet

Checker: Copyright (C) 2009 Benoît Boyer

Tabi: Copyright (C) 2003 Thomas Genet and [Boinet Matthieu, Brouard Robert, Cudennec Loic, Durieux David, Gandia Sebastien, Gillet David, Halna Frederic, Le Gall Gilles, Le Nay Judicael, Le Roux Luka, Mallah Mohamad-Tarek, Marchais Sebastien, Martin Morgane, Minier François, Stute Mathieu] -- aavisu project team for french "maitrise" level (4th University year) 2002-2003 at IFSIC/Universite de Rennes 1.

All these tools are freely available, under the terms of the GNU LIBRARY GENERAL PUBLIC LICENSE.

Distributions

The Tree Automata Completion Checker is now available. This checker certifies that a tree automaton, obtained by tree automata completion, recognizes a superset of reachable terms. It consists of Ocaml functions extracter from a Coq specification of tree automata completion. The principle is describe in the IJCAR paper that can be found here, the code can be downloaded here.
Version 3.0 is now available in source form here. This version does no longer include the tree automata library but focuses on reachability analysis and equational approximations. If you plan to perform basic tree automata manipulation, use Taml or Tabi, you need version 2.2 instead.
Version 2.2 is distributed in 2 different forms:

Older versions.

Papers about Timbuk

[BGJ08] (pdf): B. Boyer, T. Genet and T. Jensen. Certifying a Tree Automata Completion Checker. In Proceedings of IJCAR'08, volume 5195 of Lecture Notes in Computer Science. Springer-Verlag, 2008.

[FGT03] (gzipped or draft in PDF format): Guillaume Feuillade, Thomas Genet and Valérie Viet Triem Tong. Reachability Analysis of Term Rewriting Systems. Technical Report RR-4970, INRIA, 2003. (Or the corrected version To be published in Journal of Automated Reasoning, 2004)
[GT01] (gzipped or not): T. Genet and V. Viet Triem Tong. Reachability Analysis of Term Rewriting Systems with Timbuk. In Proceedings 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Havana (Cuba), volume 2250 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2001.
[Gen98a] (zipped or not): T. Genet Decidable approximations of sets of descendants and sets of normal forms. In T. Nipkow, editor, Proceedings 9th International Conference on Rewriting Techniques and Applications, Tsukuba (Japan), volume 1379 of Lecture Notes in Computer Science, pages 151-165. Springer-Verlag, 1998.