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.


References in zbMATH (referenced in 40 articles )

Showing results 1 to 20 of 40.
Sorted by year (citations)

1 2 next

  1. Felgenhauer, Bertram; Thiemann, René: Reachability, confluence, and termination analysis with state-compatible automata (2017)
  2. Genet, Thomas; Salmon, Yann: Reachability analysis of innermost rewriting (2017)
  3. Héam, P.-C.; Hugot, V.; Kouchnarenko, O.: The emptiness problem for tree automata with at least one global disequality constraint is NP-hard (2017)
  4. Genet, Thomas: Termination criteria for tree automata completion (2016)
  5. Jacquemard, Florent; Kojima, Yoshiharu; Sakai, Masahiko: Term rewriting with prefix context constraints and bottom-up strategies (2015)
  6. Vágvölgyi, Sándor: Symbol different term rewrite systems (2015)
  7. Barguñó, Luis; Creus, Carles; Godoy, Guillem; Jacquemard, Florent; Vacher, Camille: Decidable classes of tree automata mixing local and global constraints modulo flat theories (2013)
  8. Courbis, Roméo: Rewriting approximations for properties verification over CCS specifications (2012)
  9. Lengál, Ondřej; Šimáček, Jiří; Vojnar, Tomáš: VATA: a library for efficient manipulation of non-deterministic tree automata (2012)
  10. Jacquemard, Florent; Kojima, Yoshiharu; Sakai, Masahiko: Controlled term rewriting (2011)
  11. Genet, Thomas; Rusu, Vlad: Equational approximations for tree automata completion (2010)
  12. Lammich, Peter; Lochbihler, Andreas: The Isabelle collections framework (2010)
  13. Boichut, Yohan; Courbis, Romeo; Heam, Pierre-Cyrille; Kouchnarenko, Olga: Handling non left-linear rules when completing tree automata (2009)
  14. Boichut, Yohan; Héam, Pierre-Cyrille; Kouchnarenko, Olga: How to tackle integer weighted automata positivity (2009)
  15. Courbis, Roméo; Héam, Pierre-Cyrille; Kouchnarenko, Olga: TAGED approximations for temporal properties model-checking (2009)
  16. Balland, Emilie; Boichut, Yohan; Genet, Thomas; Moreau, Pierre-Etienne: Towards an efficient implementation of tree automata completion (2008)
  17. Boichut, Y.; Courbis, R.; Héam, P.-C.; Kouchnarenko, O.: Handling left-quadratic rules when completing tree automata (2008)
  18. Boichut, Y.; Héam, P.-C.: A theoretical limit for safety verification techniques with regular fix-point computations (2008)
  19. Boichut, Y.; Héam, P.-C.; Kouchnarenko, O.: Approximation-based tree regular model-checking (2008)
  20. Boichut, Yohan; Courbis, Roméo; Héam, Pierre-Cyrille; Kouchnarenko, Olga: Finer is better: Abstraction refinement for rewriting approximations (2008)

1 2 next