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.
Type de document :
Communication dans un congrès
José Meseguer and Grigore Rosu. 12th International Conference on Algebraic Methodology and Software Technology - AMAST'08, Jul 2008, Urbana, Illinois, United States. Springer, 5140, pp.67-82, 2008, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00304010
Contributeur : Emilie Balland <>
Soumis le : mercredi 24 septembre 2008 - 11:50:30
Dernière modification le : mardi 21 novembre 2017 - 15:22:11
Document(s) archivé(s) le : jeudi 4 octobre 2012 - 15:33:40

Fichier

finalversion.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00304010, version 1

Citation

Emilie Balland, Yohan Boichut, Thomas Genet, Pierre-Etienne Moreau. Towards an Efficient Implementation of Tree Automata Completion. José Meseguer and Grigore Rosu. 12th International Conference on Algebraic Methodology and Software Technology - AMAST'08, Jul 2008, Urbana, Illinois, United States. Springer, 5140, pp.67-82, 2008, Lecture Notes in Computer Science. 〈inria-00304010〉

Partager

Métriques

Consultations de la notice

465

Téléchargements de fichiers

118