Towards an Efficient Implementation of Tree Automata Completion

Emilie Balland 1 Yohan Boichut 1 Thomas Genet 2 Pierre-Etienne Moreau 1
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Term Rewriting Systems (TRSs) are now commonly used as a modeling language for applications. In those rewriting based models, reachability analysis, i.e. proving or disproving that a given term is reachable from a set of input terms, provides an efficient verification technique. Using a tree automata completion technique, it has been shown that the non reachability of a term t can be verified by computing an over- approximation of the set of reachable terms and proving that t is not in the over-approximation. Since the verification of real programs gives rise to rewrite models of significant size, efficient implementations of completion are essential. We present in this paper a TRS transformation preserving the reachability analysis by tree automata completion. This transforma- tion makes the completion implementation based on rewriting techniques possible. Thus, the reduction of a term to a state by a tree automaton is fully handled by rewriting. This approach has been prototyped in Tom, a language extension which adds rewriting primitives to Java. The first experiments are very promising relative to the state-of-the-art tool Timbuk.
Document type :
Conference papers
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download
Contributor : Emilie Balland <>
Submitted on : Wednesday, September 24, 2008 - 11:50:30 AM
Last modification on : Friday, November 16, 2018 - 1:30:27 AM
Long-term archiving on : Thursday, October 4, 2012 - 3:33:40 PM


Files produced by the author(s)


  • HAL Id : inria-00304010, version 1


Emilie Balland, Yohan Boichut, Thomas Genet, Pierre-Etienne Moreau. Towards an Efficient Implementation of Tree Automata Completion. 12th International Conference on Algebraic Methodology and Software Technology - AMAST'08, Jul 2008, Urbana, Illinois, United States. pp.67-82. ⟨inria-00304010⟩



Record views


Files downloads