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 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. See distributions below.
Tree Automata Completion Checker: 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.
TimbukCEGAR (alpha) is available! This is an (alpha) version of Timbuk taking advantage of CounterExample Guided Abstraction Refinement (a.k.a. CEGAR) for finding counterexamples or automatically refining approximations. TimbukCEGAR alpha is available in source form. Note that installing Buddy-2.4 BDD library is necessary before compiling TimbukCEGAR.The archive also contains several simple test examples as well as a Term Rewriting System produced from a Java program using Copster.
TimbukLTA (alpha) is available! This is an (alpha) version of Timbuk using Lattice Tree Automata to represent (efficiently) built-in values such as integers, strings, etc. This version is a first instance and deals with integer arithmetic. TimbukLTA is available in source form. Details can be found in this report.

Taml (Version 2.2 only): 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 (Version 2.2 only): 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)

License

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

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

TimbukCEGAR : Copyright (C) 2011 Thomas Genet, Yohan Boichut and Benoît Boyer

TimbukLTA : Copyright (C) 2012 Thomas Genet, Valérie Murat and Tristan Le Gall

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

Version 3.1 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. Old version 3.0 is here.
Version 2.2 is distributed in two different forms:
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 described in the IJCAR paper that can be found here, the code can be downloaded here.
TimbukCEGAR alpha is a prototype version available in source form. Note that installing Buddy-2.4 BDD library is necessary before compiling TimbukCEGAR.
TimbukLTA alpha is a prototype version available in source form. Details can be found in this report.

Older versions.

Papers about Timbuk

[GR10] (pdf): T. Genet and V. Rusu. Equational Tree Automata Completion. In Journal of Symbolic Computation. Volume 45. Elsevier, 2010.

[Gen09] (pdf): Thomas Genet. Reachability analysis of rewriting for software verification. Habilitation à diriger des recherches, Université de Rennes 1, 2009.

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

Related papers

[BGJL07] (pdf): Y. Boichut, T. Genet, T. Jensen and L. Le Roux. Rewriting Approximations for Fast Prototyping of Static Analyzers. In Proceedings of 18th International Conference on Rewriting Techniques and Applications, volume 4533 of Lecture Notes in Computer Science. Springer-Verlag, 2007.

[GTTT03] (gzipped): T. Genet, Y.-M. Tang-Talpin, and V. Viet Triem Tong. Verification of copy-protection cryptographic protocol using approximations of term rewriting systems. In Proc. of WITS'03, Workshop on Issues in the Theory of Security, 2003.
[OCKS02] (gzipped): F. Oehl, G. Gécé, O. Kouchnarenko, and D. Sinclair. Automatic Approximation for the Verification of Cryptographic Protocols. In Proceedings of Formal Aspects of Security (FASec'02), to appear in Lecture Notes in Computer Science, Springer-Verlag.
[OS02] (gzipped): F. Oehl and D. Sinclair. Combining ISABELLE and Timbuk for Cryptographic Protocol Verification. In Proceedings of Workshop Sécurité des Communications sur Internet (SECI 2002).
[GK00] (gzipped or not): T. Genet and F. Klay. Rewriting for Cryptographic Protocol Verification. In Proceedings 17th International Conference on Automated Deduction, Pittsburgh (Pen., USA), volume 1831 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2000.
[Gen98b] (zipped,gzipped or not): T. Genet. Contraintes d'ordre et automates d'arbres pour les preuves de terminaison. Thèse de Doctorat d'Université, Université Henri Poincaré - Nancy 1, 1998.

Bug report and comments

Do not hesitate to report any bug in the code. Please report comments, improvements and bugs to Thomas.Genet@irisa.fr

Last Modified: 2012/03/7