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, ...

• Type: Conference
• Year: 2008
• Where: AMAST
• Authors: Emilie Balland, Yohan Boichut, Thomas Genet, Pierre-Etienne Moreau
• Keywords: AMAST 2008, Reachability Analysis, Software Engineering, Term Rewriting Systems, Tree Automata Completion