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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 47 articles )

Showing results 41 to 47 of 47.
Sorted by year (citations)
  1. Zunino, Roberto; Degano, Pierpaolo: Handling exp, (\times) (and timestamps) in protocol analysis (2006)
  2. Durand, Irène: \textttAutowrite: a tool for term rewrite systems and tree automata (2005)
  3. Nesi, Monica; Rucci, Giuseppina: Formalizing and analyzing the Needham-Schroeder symmetric-key protocol by rewriting (2005)
  4. Feuillade, Guillaume; Genet, Thomas; Viet Triem Tong, Valérie: Reachability analysis over term rewriting systems (2004)
  5. Feuillade, Guillaume; Genet, Thomas: Reachability in conditional term rewriting systems (2003)
  6. Letz, Reinhold; Stenz, Gernot: Integration of equality reasoning into the disconnection calculus (2002)
  7. Genet, Thomas; Tong, Valérie Viet Triem: Reachability analysis of term rewriting systems with Timbuk (2001)