A3PAT, an Approach for Certified Automated Termination Proofs

Evelyne Contejean 1, 2 Pierre Courtieu 3 Julien Forest 3 Andrei Paskevich 1, 2 Olivier Pons 3 Xavier Urbain 1, 2, *
* Auteur correspondant
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
2 LRI - Laboratoire de Recherche en Informatique
3 CEDRIC - Centre d'étude et de recherche en informatique et communications
Abstract : Software engineering, automated reasoning, rule-based programming or specifications often use rewriting systems for which termination, among other properties, may have to be ensured. This paper presents the approach developed in Project A3PAT to discover and moreover certify, with full automation, termination proofs for term rewriting systems. It consists of two developments: the Coccinelle library formalises numerous rewriting techniques and termination criteria for the Coq proof assistant; the CiME3 rewriting tool translates termination proofs (discovered by itself or other tools) into traces that are certified by Coq assisted by Coccinelle. The abstraction level of our formalisation allowed us to weaken premises of some theorems known in the literature, thus yielding new termination criteria, such as an extension of the powerful subterm criterion (for which we propose the first full Coq formalisation). Techniques employed in CiME3 also improve on previous works on formalisation and analysis of dependency graphs.
Keywords : Automated Reasoning Formal Proof Term Rewriting Termination
Type de document :
Communication dans un congrès
John Gallagher and Janis Voigtländer. 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Jan 2010, Madrid, Spain. ACM, pp.63-72, 2010, PEPM'10. 〈10.1145/1706356.1706370〉
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00535655
Contributeur : Andrei Paskevich <>
Soumis le : vendredi 12 novembre 2010 - 11:46:23
Dernière modification le : mardi 13 novembre 2018 - 17:10:02
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 15:30:40

Fichier

pepm10-contejean.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | UMR8623 | LRI-VALS | UNIV-HESAM

Citation

Evelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons, et al.. A3PAT, an Approach for Certified Automated Termination Proofs. John Gallagher and Janis Voigtländer. 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Jan 2010, Madrid, Spain. ACM, pp.63-72, 2010, PEPM'10. 〈10.1145/1706356.1706370〉. 〈inria-00535655〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

266

Téléchargements de fichiers

147

Contact


archive-ouverte@inria.fr