Timbuk


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 available tools are:

 

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

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 TA4SP -- a cryptographic protocol verification tool -- developped by Yohan Boichut.

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
 
 
 
 
 
irisa
Istic
Universite Rennes1


Last Modified: 2012/03/7