Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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.
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Thomas Genet Connect in order to contact the contributor
Submitted on : Monday, April 7, 2008 - 10:05:06 AM
Last modification on : Thursday, October 27, 2022 - 3:44:48 AM
Long-term archiving on: : Friday, November 25, 2016 - 9:44:57 PM


Files produced by the author(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⟩



Record views


Files downloads