Abstract
Nowadays, formal methods rely on tools of different kinds: proof assistants with which the user interacts to discover a proof step by step; and fully automated tools which make use of (intricate) decision procedures. But while some proof assistants can check the soundness of a proof, they lack automation. Regarding automated tools, one still has to be satisfied with their answers Yes/No/Do not know, the validity of which can be subject to question, in particular because of the increasing size and complexity of these tools.
In the context of rewriting techniques, we aim at bridging the gap between proof assistants that yield formal guarantees of reliability and highly automated tools one has to trust. We present an approach making use of both shallow and deep embeddings. We illustrate this approach with a prototype based on the CiME rewriting toolbox, which can discover involved termination proofs that can be certified by the Coq proof assistant, using the Coccinelle library for rewriting.
Work partially supported by A3PAT project of the French ANR (ANR-05-BLAN-0146-01).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. J. Autom. Reasoning 29(3-4), 253–275 (2002)
Blanqui, F., Coupet-Grimal, S., Delobel, W., Hinderer, S., Koprowski, A.: Color, a coq library on rewriting and termination. In: Geser and Sondergaard [16]
Contejean, E.: A certified AC matching algorithm. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 70–84. Springer, Heidelberg (2004)
Contejean, E.: Coccinelle (2005), http://www.lri.fr/~contejea/Coccinelle/coccinelle.html
Contejean, E., Corbineau, P.: Reflecting proofs in first-order logic with equality. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 7–22. Springer, Heidelberg (2005)
Contejean, E., Marché, C., Monate, B., Urbain, X.: Proving termination of rewriting with cime. In: Rubio [27], pp. 71–73, http://cime.lri.fr
Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG-88. LNCS, vol. 417, Springer, Heidelberg (1990)
Dershowitz, N.: Orderings for term rewriting systems. Theoretical Computer Science 17(3), 279–301 (1982)
Dershowitz, N.: Termination of rewriting. Journal of Symbolic Computation 3(1), 69–115 (1987)
Dershowitz, N.: Termination Dependencies. In: Rubio [27] Technical Report DSIC II/15/03, Univ. Politécnica de Valencia, Spain
Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–320. North-Holland, Amsterdam (1990)
Doligez, D.: Zenon. http://focal.inria.fr/zenon/
Endrullis, J.: Jambox, http://joerg.endrullis.de/index.html .
Geser, A., Sondergaard, H. (eds.).: Extended Abstracts of the 8th International Workshop on Termination, WST 2006 (August 2006)
Giesl, J., Schneider-Kamp, P., Thiemann, R.: Aprove 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, Springer, Heidelberg (2006)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and Improving Dependency Pairs. Journal of Automated Reasoning 37(3), 155–203 (2006)
Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 32–46. Springer, Heidelberg (2003)
Hirokawa, N., Middeldorp, A.: Tyrolean termination tool. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 175–184. Springer, Heidelberg (2005)
Hubert, T.: Certification des preuves de terminaison en Coq. Rapport de DEA, Université Paris 7, In French (September 2004)
Koprowski, A.: TPA, http://www.win.tue.nl/tpa
Lankford, D.S.: Onproving term rewriting systems are Noetherian.Technical Report MTP-3, Mathematics Department, Louisiana Tech. Univ., (1979) Available at http://perso.ens-lyon.fr/pierre.lescanne/not_accessible.html
Marché, C., Zantema, H.: The termination competition 2006. In Geser and Sondergaard [16], http://www.lri.fr/~marche/termination-competition/
Nguyen, Q.H., Kirchner, C., Kirchner, H.: External rewriting for skeptical proof assistants. J. Autom. Reasoning 29(3-4), 309–336 (2002)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. In: Nipkow, T., Paulson, L.C., Wenzel, M. (eds.) Isabelle/HOL. LNCS, vol. 2283, Springer, Heidelberg (2002)
Rubio, A., (ed.).: Extended Abstracts of the 6th International Workshop on Termination, WST 2003, Technical Report DSIC II/15/03, Univ. Politécnica de Valencia, Spain (June 2003)
The Coq Development Team. The Coq Proof Assistant Documentation – Version V8.1 (February 2007), http://coq.inria.fr .
Urbain, X.: Modular and incremental automated termination proofs. Journal of Automated Reasoning 32, 315–355 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X. (2007). Certification of Automated Termination Proofs. In: Konev, B., Wolter, F. (eds) Frontiers of Combining Systems. FroCoS 2007. Lecture Notes in Computer Science(), vol 4720. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74621-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-74621-8_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74620-1
Online ISBN: 978-3-540-74621-8
eBook Packages: Computer ScienceComputer Science (R0)