Adapting proof automation to adapt proofs

Talia Ringer, John Leo, Nathaniel Yazdani, Dan Grossman

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish (US)
Title of host publicationCPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018
EditorsAmy Felty, June Andronick
PublisherAssociation for Computing Machinery, Inc
Pages115-129
Number of pages15
ISBN (Electronic)9781450355865
DOIs
StatePublished - Jan 8 2018
Externally publishedYes
Event7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 - Los Angeles, United States
Duration: Jan 8 2018Jan 9 2018

Conference

Conference7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018
Country/TerritoryUnited States
CityLos Angeles
Period1/8/181/9/18

Keywords

  • Proof automation
  • Proof evolution
  • Proof repair

ASJC Scopus subject areas

  • Computer Science Applications
  • Software

Fingerprint

Dive into the research topics of 'Adapting proof automation to adapt proofs'. Together they form a unique fingerprint.

Cite this