Certifying a Tree Automata Completion Checker

Benoît Boyer (1) , Thomas Genet (1) , Thomas Jensen (1)

1 Lande - Logiciel : ANalyse et DEveloppement

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.

Mots clés: Term Rewriting Systems; Tree Automata; Tree Automata Completion; Certification; Coq; Reachability

Domaines: Logique en informatique [cs.LO]; Génie logiciel [cs.SE]

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