References

1999–2003  (Barras et al.)

B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliâtre, 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 7.4. Rapport technique, INRIA, France, 1999–2003. http://coq.inria.fr/doc/main.html.

2001  (Blanchet)

B. Blanchet. An efficient cryptographic protocol verifier based on Prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82–96. IEEE Computer Society Press, 2001.

1996  (Boudet and Comon)

A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In H. Kirchner, editor, Colloquium on Trees in Algebra and Programming (CAAP'96), pages 30–43. Springer Verlag LNCS 1059, 1996.

1996  (Devienne et al.)

P. Devienne, P. Lebègue, A. Parrain, J.-C. Routier, and J. Würtz. Smallest Horn clause programs. Journal of Logic Programming, 27 (3): 227–267, 1996. URL citeseer.nj.nec.com/devienne94smallest.html.

1991  (Frühwirth et al.)

T. Frühwirth, E. Shapiro, M. Y. Vardi, and E. Yardeni. Logic programs as types for logic programs. In Proc. 6th Symp Logic in Computer Science, pages 300–309, 1991.

2005  (Goubault-Larrecq)

J. Goubault-Larrecq. Deciding H₁ by resolution. Information Processing Letters, 95 (3): 401–408, Aug. 2005. URL http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Goubault-h1.pdf.

2004  (Goubault-Larrecq)

J. Goubault-Larrecq. Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve ? In Actes 15èmes journées francophones sur les langages applicatifs (JFLA'04), Sainte-Marie-de-Ré, France, Jan. 2004, pages 1–20. INRIA, collection didactique, 2004. URL http://www.lsv.ens-cachan.fr/Publis/PAPERS/JGL-JFLA2004.ps.

2005  (Goubault-Larrecq and Parrennes)

J. Goubault-Larrecq and F. Parrennes. Cryptographic protocol analysis on real C code. In R. Cousot, editor, Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 of Lecture Notes in Computer Science, Paris, France, Jan. 2005. Springer. URL http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf. To appear.

2002  (Nielson et al.)

F. Nielson, H. R. Nielson, and H. Seidl. Normalizable Horn clauses, strongly recognizable relations and Spi. In 9th Static Analysis Symposium (SAS). Springer Verlag LNCS 2477, 2002.

1986  (Pelletier)

F. J. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2: 191–216, 1986.

2001  (Selinger)

P. Selinger. Models for an adversary-centric protocol logic. Electronic Notes in Theoretical Computer Science, 55 (1): 73–87, 2001. Proceedings of the 1st Workshop on Logical Aspects of Cryptographic Protocol Verification (LACPV'01), J. Goubault-Larrecq, ed.

2002  (Suttner and Sutcliffe)

C. B. Suttner and G. Sutcliffe. The TPTP problem library v2.5.0, 2002. URL http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml.