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 used to
verify Java programs and 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 available
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: This is a 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: This is a 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 paper.
- TimbukStrat (alpha) is
available! This is an (alpha) version of Timbuk computing
approximation of reachable terms for the innermost
rewriting strategy. TimbukStrat is available in source
form. Note
that installing Buddy-2.4
BDD library is necessary before compiling TimbukStrat.The archive also
contains several simple test examples. 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
TimbukStrat : Copyright (C) 2013 Thomas Genet and
Yann Salmon
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
- [GLLGM13] (pdf)
- T. Genet, T. Le Gall, A. Legay and V. Murat.A Completion Algorithm for Lattice Tree Automata.
In Proceedings of CIAA'13, volume 7982 of Lecture Notes
in Computer Science, pages 134-145. Springer-Verlag, 2013.
- [BBGL12] (pdf)
- Y. Boichut, B. Boyer, T. Genet and A. Legay. Equational Abstraction Refinement for Certified Tree Regular Model Checking.
In Proceedings of ICFEM'12, volume 7635 of Lecture Notes
in Computer Science, pages 299-315. Springer-Verlag, 2012.
- [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.
Related links
The Tree Automata Techniques and
Application (TATA)
home page.
Timbuk is used as a back-end prover in AVISPA
a cryptographic protocol verification tool.
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