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 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 implementation of completion, usable with any approximation performed during completion, small and fast. Some benchmarks are given to show how efficient the tool is.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., Héam, P.-C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santos Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: Natural deduction with general elimination rules. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 541–567. Springer, Heidelberg (2005)
Ballad, E., Boichut, Y., Genet, T., Moreau, P.-E.: Towards an Efficient Implementation of Tree Automata Completion. In: AMAST 2008 (to be published, 2008)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)
Barthe, G., Dufay, G.: A tool-assisted framework for certified bytecode verification. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 99–113. Springer, Heidelberg (2004)
Boyer, B., Genet, T., Jensen, T.: Certifying a Tree Automata Completion Checker. Technical Report RR 6462, INRIA (2008), http://hal.inria.fr/inria-00258275/fr/
Boichut, Y., Genet, T., Jensen, T., Leroux, L.: Rewriting Approximations for Fast Prototyping of Static Analyzers. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 48–62. Springer, Heidelberg (2007)
Boichut, Y., Héam, P.-C., Kouchnarenko, O.: Automatic Approximation for the Verification of Cryptographic Protocols. In: Proc. AVIS 2004, joint to ETAPS 2004, Barcelona (Spain) (2004)
Besson, F., Jensen, T., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci. 364(3), 273–291 (2006)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2002), http://www.grappa.univ-lille3.fr/tata/
Cachera, D., Jensen, T., Pichardie, P., Rusu, V.: Extracting a data flow analyser in constructive logic. Theor. Comput. Sci. 342(1), 56–78 (2005)
Feuillade, G., Genet, T., Viet Triem Tong, V.: Reachability Analysis over Term Rewriting Systems. JAR 33(3-4), 341–383 (2004)
Genet, T.: Decidable approximations of sets of descendants and sets of normal forms (extended version). Technical Report RR-3325, INRIA (1997)
Genet, T.: Decidable approximations of sets of descendants and sets of normal forms. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 151–165. Springer, Heidelberg (1998)
Genet, T., Klay, F.: Rewriting for Cryptographic Protocol Verification. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831. Springer, Heidelberg (2000)
Gilleron, R., Tison, S.: Regular tree languages and rewrite systems. Fundamenta Informaticae 24, 157–175 (1995)
Genet, T., Tang-Talpin, Y.-M., Viet Triem Tong, V.: Verification of Copy Protection Cryptographic Protocol using Approximations of Term Rewriting Systems. In: WITS 2003 (2003)
Genet, T., Viet Triem Tong, V.: Timbuk 2.0 – a Tree Automata Library. IRISA / Université de Rennes 1 (2000), http://www.irisa.fr/lande/genet/timbuk/
Jacquemard, F.: Decidable approximations of term rewriting systems. In: Ganzinger, H. (ed.) Proc. 7th RTA Conf., New Brunswick (New Jersey, USA), pp. 362–376. Springer, Heidelberg (1996)
Klein, G., Nipkow, T.: Verified bytecode verifiers. TCS 298 (2003)
Letouzey, P., Théry, L.: Formalizing stalmarck’s algorithm in coq. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869. Springer, Heidelberg (2000)
Rety, P.: Regular Sets of Descendants for Constructor-based Rewrite Systems. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol. 1705. Springer. Heidelberg (1999)
Rival, X., Goubault-Larrecq, J.: Experiments with finite tree automata in coq. In: Proc. of TPHOL 2001. LNCS. Springer, Heidelberg (2001)
Takai, T.: A Verification Technique Using Term Rewriting Systems and Abstract Interpretation. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 119–133. Springer, Heidelberg (2004)
Zunino, R., Degano, P.: Handling exp, × (and timestamps) in protocol analysis. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006 and ETAPS 2006. LNCS, vol. 3921, pp. 413–427. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boyer, B., Genet, T., Jensen, T. (2008). Certifying a Tree Automata Completion Checker. In: Armando, A., Baumgartner, P., Dowek, G. (eds) Automated Reasoning. IJCAR 2008. Lecture Notes in Computer Science(), vol 5195. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71070-7_43
Download citation
DOI: https://doi.org/10.1007/978-3-540-71070-7_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71069-1
Online ISBN: 978-3-540-71070-7
eBook Packages: Computer ScienceComputer Science (R0)