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 Higher-Order Functional Programs, Java programs and Cryptographic Protocols (see some papers and in the examples of the distribution).
Current version Timbuk 3.2 provides:
- the 'timbuk' command for tree automata completion
(optimized). Now permits to define initial sets of terms using
(Simplified) tree
Regular Expressions and can automatically generate equations for
functional TRS.
- 'taml' which is an OCaml interpreter equipped with the completion
functions and all the necessary functions to manipulate tree
automata (unoptimized):
- Tree automata parsing and manipulations: intersection, union,
cleaning, emptiness decision, determinisation, inclusion, equality;
- Tree Regular expression parsing and manipulations;
- Conversion between tree regular expressions and tree
automata, and vice versa (using the algorithms coming from this
paper and
from this one);
- Matching of Term Rewriting Systems over tree automata,
etc.
If you are looking for older or specific versions of Timbuk like: TimbukCEGAR, TimbukStrat,
TimbukLTA, or the Tree Automata Completion Checker have a look here.
How to use Timbuk?
- Download and compile the source
version of Timbuk 3.2. See the README file in the
archive for compilation and installation instructions. You will
need a full OCaml compiler and OCamlbuild.
- Use the online version. Requires no
installation but it may take some time to start!
- Use the code of the online version... offline: download
the archive, uncompress it, and open
the index.html file of the TimbukOnLine folder in your browser.
Timbuk 3.2 : Copyright (C) 2017 Thomas Genet,
Yohan
Boichut, Benoît Boyer, Tristan
Gillard, Timothée
Haudebourg and Sébastien Lê Cong.
TimbukOnLine by Timothée Haudebourg.
Timbuk is freely available, under the terms of the GNU LIBRARY GENERAL PUBLIC LICENSE.
Papers
about Timbuk
- [Genet16] (pdf)
- T. Genet. Termination Criteria for Tree Automata
Completion. In Journal of Logical and Algebraic Methods in Programming.
Volume 85, Issue 1, Part 1, pages 3-33. 2016.
- [GS15] (pdf)
- T. Genet and Y. Salmon. Reachability Analysis of
Innermost Rewriting.
In Proceedings of RTA'15. LIPIcs 36, Schloss
Dagstuhl. 2015.
- [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.
Specific versions of Timbuk and related tools are
- 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: This is a 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.
- Older versions.
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-2017 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.
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: 2017/06/26