Timbuk Reachability Analysis and Tree Automata Calculations

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 (TRS) 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).

Timbuk exists in two flavours

Timbuk 4 is specialized for functional program analysis (needs CVC4).

Targets higher-order functional programs encoded into TRS.
Proves structural properties on algebraic data types manipulated by such programs.
Tree automata proving such properties are built automatically.

Here is the source distribution and the results of some experiments on functional program automatic verification.

Timbuk 3.2 generic reachability analysis tool and tree automata library.

General purpose tree automata library implementing all well-known algorithms.
Conversion between tree regular expressions and tree automata, and vice versa (using the algorithms coming from this paper and from this one).
Reachability analysis on TRS using both automatic and manual definition of approximations.

See below for installation instructions or use it in your browser

. This requires no installation but takes some time to start!

There are also specific versions of Timbuk like: TimbukCEGAR, TimbukStrat, TimbukLTA, or the Tree Automata Completion Checker have a look here.

How to use Timbuk 3.2?

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 '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.
Use the 'taml' command for 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.

Alternative : Timbuk 3.2 in your browser

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

[Gen18] (pdf): T. Genet. Completeness of Tree Automata Completion. In Proceedings of FSCD'18. Volume 108 of LIPIcs, Schloss Dagstuhl. 2018.
[GGHL18] (pdf): T. Genet, T. Gillard, T. Haudebourg, S. Lê Cong. Extending Timbuk to Verify Functional Programs. In Proceedings of WRLA'18, To be published. Springer-Verlag, 2018.
[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

[HGJ20] (pdf): T. Haudebourg, T. Genet and T. Jensen. Regular Language Type Inference with Term Rewriting. In Proceedings of ICFP'20. ACM, 2020.
[GHJ18] (pdf): T. Genet, T. Haudebourg and T. Jensen. Verifying Higher-Order Functions with Tree Automata. In Proceedings of FoSSaCS'18. Volume 10803 Lecture Notes in Computer Science. Springer Verlag, 2018.
[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.

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

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: 2021/04/06