Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Reachability Analysis of Term Rewriting Systems with Timbuk

Thomas Genet 1 Valérie Viet Triem Tong 1 
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : We present Timbuk - a tree automata library - which implements usual operation- s on tree automata as well as a completion algorithm used to compute an over-approximation of the set of descendants R*(E) for a regular set E and a term rewriting system R, possibly non linear and non terminating. On several examples of term rewriting systems representing programs and systems to verify, we show how to use Timbuk to construct their approximations and then prove unreachability properties of these systems.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 8:23:55 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:27 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:03:44 PM


  • HAL Id : inria-00072321, version 1


Thomas Genet, Valérie Viet Triem Tong. Reachability Analysis of Term Rewriting Systems with Timbuk. [Research Report] RR-4266, INRIA. 2001. ⟨inria-00072321⟩



Record views


Files downloads