Experiments with Finite Tree Automata in Coq

1. B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliatre, E. Giménez, H. Herbelin, G. Huet, C. Muñoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saibi, and B. Werner. The Coq proof assistant reference manual: Version 6.3.1. Technical report, INRIA, France, 1999.

   Google Scholar 

2. S. Boutin. Using reflection to build efficient and certified decision procedures. In M. Abadi and T. Ito, editors, TACS’97. Springer-Verlag LNCS 1281, 1997.

   Google Scholar 

3. R. Boyer and J. S. Moore. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In The Correctness Problem in Computer Science. Acad. Press, 1981.

   Google Scholar 

4. W. Charatonik and A. Podelski. Set-based analysis of reactive infinite-state systems. In B. Steffen, editor, TACAS’98, pages 358–375. Springer Verlag LNCS 1384, 1998.

   Google Scholar 

5. H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, T. Sophie, and M. Tommasi. Tree automata techniques and applications. Available at http://www.grappa.univ-lille3.fr/tata, 1997.

6. L. Fribourg and M. Veloso Peixoto. Automates concurrents à contraintes. Technique et Science Informatique, 13(6):837–866, 1994.

   MATH  Google Scholar 

7. F. Gécseg and M. Steinby. Tree languages. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 3, pages 1–68. Springer Verlag, 1997.

   Google Scholar 

8. J. Goubault-Larrecq. Satisfiability of inequality constraints and detection of cycles with negative weight in graphs. Part of the Coq contribs, available at http://pauillac.inria.fr/coq/contribs/graphs.html, 1998.

9. J. Goubault-Larrecq. A method for automatic cryptographic protocol verification. In FMPPTA’2000, pages 977–984. Springer Verlag LNCS 1800, 2000.

   Google Scholar 

10. J. Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38:162–170, 1995.

    Article  MathSciNet  Google Scholar 

11. J. Harrison. Stålmarck’s algorithm as a HOL derived rule. In J. von Wright, J. Grundy, and J. Harrison, editors, TPHOL’96, pages 221–234. Springer Verlag LNCS 1125, 1996.

    Google Scholar 

12. J.-P. Jouannaud. Rewrite proofs and computations. In H. Schwichtenberg, editor, Proof and Computation, volume 139 of NATO series F: Computer and Systems Sciences, pages 173–218. Springer Verlag, 1995.

    Google Scholar 

13. D. Monniaux. Abstracting cryptographic protocols with tree automata. In SAS’99, pages 149–163. Springer Verlag LNCS 1694, 1999.

    Google Scholar 

14. O. Müller. A verification environment for I/O automata based on formalized meta-theory. Master’s thesis, Technische Universität München, 1998.

    Google Scholar 

15. W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 4, pages 133–191. Elsevier Science Publishers B. V., 1990.

    Google Scholar 

16. K. N. Verma, J. Goubault-Larrecq, S. Prasad, and S. Arun-Kumar. Reflecting BDDs in Coq. In ASIAN’2000, pages 162–181. Springer Verlag LNCS 1961, 2000.

    Google Scholar 

17. R. W. Weyhrauch. Prolegomena to a theory of mechanized formal reasoning. Artifical Intelligence, 13(1, 2):133–170, 1980.

    Article  MATH  MathSciNet  Google Scholar 

18. S. Yu and Z. Luo. Implementing a model checker for LEGO. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, FME’97, pages 442–458. Springer-Verlag LNCS 1313, 1997.

    Google Scholar 

Download references