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

Showing results 21 to 40 of 47.
Sorted by year (citations)
  1. Courbis, Roméo; Héam, Pierre-Cyrille; Kouchnarenko, Olga: TAGED approximations for temporal properties model-checking (2009)
  2. Balland, Emilie; Boichut, Yohan; Genet, Thomas; Moreau, Pierre-Etienne: Towards an efficient implementation of tree automata completion (2008)
  3. Boichut, Y.; Courbis, R.; Héam, P.-C.; Kouchnarenko, O.: Handling left-quadratic rules when completing tree automata (2008)
  4. Boichut, Y.; Héam, P.-C.: A theoretical limit for safety verification techniques with regular fix-point computations (2008)
  5. Boichut, Y.; Héam, P.-C.; Kouchnarenko, O.: Approximation-based tree regular model-checking (2008)
  6. Boichut, Yohan; Courbis, Roméo; Héam, Pierre-Cyrille; Kouchnarenko, Olga: Finer is better: Abstraction refinement for rewriting approximations (2008)
  7. Delzanno, Giorgio; Montagna, Roberto: Reachability analysis of fragments of mobile ambients in AC term rewriting (2008)
  8. Héam, P.-C.: A note on partially ordered tree automata (2008)
  9. Hendrix, Joe; Ohsaki, Hitoshi: Combining equational tree automata over AC and ACI theories (2008)
  10. Boichut, Yohan; Genet, Thomas; Jensen, Thomas; Le Roux, Luka: Rewriting approximations for fast prototyping of static analyzers (2007)
  11. Escobar, Santiago; Meseguer, José: Symbolic model checking of infinite-state systems using narrowing (2007)
  12. Escobar, Santiago; Meseguer, José; Thati, Prasanna: Narrowing and rewriting logic: from foundations to applications (2007)
  13. Geser, Alfons; Hofbauer, Dieter; Waldmann, Johannes; Zantema, Hans: On tree automata that certify termination of left-linear term rewriting systems (2007)
  14. Meseguer, José; Thati, Prasanna: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols (2007)
  15. Yorsh, Greta; Rabinovich, Alexander; Sagiv, Mooly; Meyer, Antoine; Bouajjani, Ahmed: A logic of reachable patterns in linked data-structures (2007)
  16. Boichut, Y.; Héam, P.-C.; Kouchnarenko, O.: Handling algebraic properties in automatic analysis of security protocols (2006)
  17. Boichut, Yohan; Genet, Thomas: Feasible trace reconstruction for rewriting approximations (2006)
  18. May, Jonathan; Knight, Kevin: Tiburon: a weighted tree automata toolkit (2006)
  19. Nesi, Monica; Nocera, Giustina: Deriving the type flaw attacks in the Otway-Rees protocol by rewriting (2006)
  20. Vágvölgyi, Sándor: Descendants of a recognizable tree language for sets of linear monadic term rewrite rules (2006)