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 metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/inria-00258275
Contributor : Thomas Genet <>
Submitted on : Monday, April 7, 2008 - 10:05:06 AM
Last modification on : Friday, November 16, 2018 - 1:24:48 AM
Long-term archiving on : Friday, November 25, 2016 - 9:44:57 PM

File

report.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00258275, version 3

Citation

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

Share

Metrics

Record views

377

Files downloads

164