Certifying a Tree Automata Completion Checker

9 years 2 months ago
Certifying a Tree Automata Completion Checker
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 analyzers. 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 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 has been defined so as to avoid the exponential blow up. The obtained checker is certified in Coq, independent of the implementat...
Benoît Boyer, Thomas Genet, Thomas P. Jensen
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Benoît Boyer, Thomas Genet, Thomas P. Jensen
Comments (0)