Abstract
We extend proof automation in an interactive theorem prover to analyze changes in specifications and proofs. Our approach leverages the history of changes to specifications and proofs to search for a patch that can be applied to other specifications and proofs that need to change in analogous ways. We identify and implement five core components that are key to searching for a patch. We build a patch finding procedure from these components, which we configure for various classes of changes. We implement this procedure in a Coq plugin as a proof-of-concept and use it on real Coq code to change specifications, port definitions of a type, and update the Coq standard library. We show how our findings help drive a future that moves the burden of dealing with the brittleness of small changes in an interactive theorem prover away from the programmer and into automated tooling.
Original language | English (US) |
---|---|
Title of host publication | CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018 |
Editors | Amy Felty, June Andronick |
Publisher | Association for Computing Machinery |
Pages | 115-129 |
Number of pages | 15 |
ISBN (Electronic) | 9781450355865 |
DOIs | |
State | Published - Jan 8 2018 |
Externally published | Yes |
Event | 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 - Los Angeles, United States Duration: Jan 8 2018 → Jan 9 2018 |
Conference
Conference | 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 |
---|---|
Country/Territory | United States |
City | Los Angeles |
Period | 1/8/18 → 1/9/18 |
Keywords
- Proof automation
- Proof evolution
- Proof repair
ASJC Scopus subject areas
- Computer Science Applications
- Software