Certifying a Tree Automata Completion Checker

Benoît Boyer 1 Thomas Genet 1 Thomas Jensen 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Tree automata completion is a technique for the verification of infinite state systems. It has already been used for the verification of cryptographic protocols and the prototyping of Java static analysers. However, as for many other verification techniques, the correctness of the associated tool becomes more and more difficult to guarantee. It is due to the size of the implementation that constantly grows and due to low level optimizations which are necessary to scale up the efficiency of the tool to verify real-size systems. In this paper, we define and develop a checker for tree automata produced by completion. The checker is defined using Coq and its implementation is automatically extracted from its formal specification. Using extraction gives a checker that can be run independently of the Coq environment. A specific algorithm for tree automata inclusion checking have been defined so as to avoid the exponential blow up. The obtained checker is certified in Coq, independant of the implementation of completion, usable with any approximation performed during completion, small and fast. Some benchmarks are given to illustrate the efficiency of the tool.
Type de document :
[Research Report] RR-6462, INRIA. 2008, pp.26
Liste complète des métadonnées

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

Contributeur : Thomas Genet <>
Soumis le : lundi 7 avril 2008 - 10:05:06
Dernière modification le : vendredi 16 novembre 2018 - 01:24:48
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 21:44:57


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00258275, version 3


Benoît Boyer, Thomas Genet, Thomas Jensen. Certifying a Tree Automata Completion Checker. [Research Report] RR-6462, INRIA. 2008, pp.26. 〈inria-00258275v3〉



Consultations de la notice


Téléchargements de fichiers