Timbuk
swMATH ID: | 6351 |
Software Authors: | Genet, Thomas; Boichut, Yohan; Boyer, Benoît; Tong, Valérie Viet Triem; et al. |
Description: | 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. |
Homepage: | http://www.irisa.fr/celtique/genet/timbuk/ |
Keywords: | Term Rewriting Systems |
Related Software: | Maude; AVISPA; ELAN; Isabelle; OCaml; Isabelle/HOL; AProVE; Tyrolean; MONA; JavaFAN; z3; Maude-NPA; NRL; LETHAL; HERMES; K Prover; DCTP; Nagoya Termination Tool; NaTT; MU-TERM |
Cited in: | 49 Documents |
all
top 5
Cited by 58 Authors
all
top 5
Cited in 13 Serials
Cited in 4 Fields
49 | Computer science (68-XX) |
6 | Mathematical logic and foundations (03-XX) |
5 | Information and communication theory, circuits (94-XX) |
2 | General algebraic systems (08-XX) |