Sciweavers

Share
AMAST
2008
Springer

Towards an Efficient Implementation of Tree Automata Completion

8 years 4 months ago
Towards an Efficient Implementation of Tree Automata Completion
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 overapproximation 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 transformation 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, ...
Emilie Balland, Yohan Boichut, Thomas Genet, Pierr
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where AMAST
Authors Emilie Balland, Yohan Boichut, Thomas Genet, Pierre-Etienne Moreau
Comments (0)
books