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...

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Benoît Boyer, Thomas Genet, Thomas P. Jensen
• Keywords: Automated Reasoning, CADE 2008, Infinite State Systems, Java Static Analyzers, Tree Automata