Paper Info
Title
A3PAT, an approach for certified automated termination proofs
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.
Year
DOI
Venue
2010
10.1145/1706356.1706370
PEPM
Keywords
Field
DocType
termination,software engineering,automated reasoning,theory,formal proof
Automated reasoning,Programming language,Computer science,Automation,Theoretical computer science,Mathematical proof,Rewriting,Abstraction layer,Certification,Proof assistant,Formal proof
Conference
Citations 
PageRank 
References 
17
0.74
30
Authors
6
Name
Order
Citations
PageRank
Evelyne Contejean131523.89
Andrei Paskevich222916.43
Xavier Urbain328616.54
Pierre Courtieu416212.55
Olivier Pons5663.05
Julien Forest61167.30