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 34 articles )

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

1 2 next

  1. Genet, Thomas; Salmon, Yann: Reachability analysis of innermost rewriting (2017)
  2. 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)
  3. Jacquemard, Florent; Kojima, Yoshiharu; Sakai, Masahiko: Term rewriting with prefix context constraints and bottom-up strategies (2015)
  4. Vágvölgyi, Sándor: Symbol different term rewrite systems (2015)
  5. Barguñó, Luis; Creus, Carles; Godoy, Guillem; Jacquemard, Florent; Vacher, Camille: Decidable classes of tree automata mixing local and global constraints modulo flat theories (2013)
  6. Courbis, Roméo: Rewriting approximations for properties verification over CCS specifications (2012)
  7. Lengál, Ondřej; Šimáček, Jiří; Vojnar, Tomáš: VATA: a library for efficient manipulation of non-deterministic tree automata (2012)
  8. Genet, Thomas; Rusu, Vlad: Equational approximations for tree automata completion (2010)
  9. Boichut, Yohan; Courbis, Romeo; Heam, Pierre-Cyrille; Kouchnarenko, Olga: Handling non left-linear rules when completing tree automata (2009)
  10. Courbis, Roméo; Héam, Pierre-Cyrille; Kouchnarenko, Olga: TAGED approximations for temporal properties model-checking (2009)
  11. Balland, Emilie; Boichut, Yohan; Genet, Thomas; Moreau, Pierre-Etienne: Towards an efficient implementation of tree automata completion (2008)
  12. Boichut, Y.; Courbis, R.; Héam, P.-C.; Kouchnarenko, O.: Handling left-quadratic rules when completing tree automata (2008)
  13. Boichut, Y.; Héam, P.-C.: A theoretical limit for safety verification techniques with regular fix-point computations (2008)
  14. Boichut, Y.; Héam, P.-C.; Kouchnarenko, O.: Approximation-based tree regular model-checking (2008)
  15. Boichut, Yohan; Courbis, Roméo; Héam, Pierre-Cyrille; Kouchnarenko, Olga: Finer is better: Abstraction refinement for rewriting approximations (2008)
  16. Delzanno, Giorgio; Montagna, Roberto: Reachability analysis of fragments of mobile ambients in AC term rewriting (2008)
  17. Héam, P.-C.: A note on partially ordered tree automata (2008)
  18. Hendrix, Joe; Ohsaki, Hitoshi: Combining equational tree automata over AC and ACI theories (2008)
  19. Boichut, Yohan; Genet, Thomas; Jensen, Thomas; Le Roux, Luka: Rewriting approximations for fast prototyping of static analyzers (2007)
  20. Escobar, Santiago; Meseguer, José: Symbolic model checking of infinite-state systems using narrowing (2007)

1 2 next