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
Complete list of metadatas

https://hal.inria.fr/inria-00072321
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 8:23:55 PM
Last modification on : Thursday, December 13, 2018 - 8:06:02 PM
Long-term archiving on : Sunday, April 4, 2010 - 11:03:44 PM

Identifiers

  • HAL Id : inria-00072321, version 1

Citation

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

Share

Metrics

Record views

168

Files downloads

574