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

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

1 2 3 next

  1. Meseguer, José: Generalized rewrite theories, coherence completion, and symbolic methods (2020)
  2. Jacquemard, Florent; Rusinowitch, Michael: One-variable context-free hedge automata (2019)
  3. Vágvölgyi, Sándor: Some decidability results on one-pass reductions (2019)
  4. Genet, Thomas: Completeness of tree automata completion (2018)
  5. Vágvölgyi, Sándor: Descendants of a recognizable tree language for prefix constrained linear monadic term rewriting with position cutting strategy (2018)
  6. Felgenhauer, Bertram; Thiemann, René: Reachability, confluence, and termination analysis with state-compatible automata (2017)
  7. Genet, Thomas; Salmon, Yann: Reachability analysis of innermost rewriting (2017)
  8. 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)
  9. Genet, Thomas: Termination criteria for tree automata completion (2016)
  10. Jacquemard, Florent; Kojima, Yoshiharu; Sakai, Masahiko: Term rewriting with prefix context constraints and bottom-up strategies (2015)
  11. Vágvölgyi, Sándor: Symbol different term rewrite systems (2015)
  12. Barguñó, Luis; Creus, Carles; Godoy, Guillem; Jacquemard, Florent; Vacher, Camille: Decidable classes of tree automata mixing local and global constraints modulo flat theories (2013)
  13. Courbis, Roméo: Rewriting approximations for properties verification over CCS specifications (2012)
  14. Lengál, Ondřej; Šimáček, Jiří; Vojnar, Tomáš: VATA: a library for efficient manipulation of non-deterministic tree automata (2012)
  15. Jacquemard, Florent; Kojima, Yoshiharu; Sakai, Masahiko: Controlled term rewriting (2011)
  16. Genet, Thomas; Rusu, Vlad: Equational approximations for tree automata completion (2010)
  17. Lammich, Peter; Lochbihler, Andreas: The Isabelle collections framework (2010)
  18. Boichut, Yohan; Courbis, Romeo; Heam, Pierre-Cyrille; Kouchnarenko, Olga: Handling non left-linear rules when completing tree automata (2009)
  19. Boichut, Yohan; Héam, Pierre-Cyrille; Kouchnarenko, Olga: How to tackle integer weighted automata positivity (2009)
  20. Boichut, Yohan; Héam, Pierre-Cyrille; Kouchnarenko, Olga: Tree automata for detecting attacks on protocols with algebraic cryptographic primitives (2009)

1 2 3 next