Adapting proof automation to adapt proofs

Talia Ringer; John Leo; Nathaniel Yazdani; Dan Grossman

doi:10.1145/3167094

Adapting proof automation to adapt proofs

Talia Ringer, John Leo, Nathaniel Yazdani, Dan Grossman

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 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	https://doi.org/10.1145/3167094
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

Online availability

10.1145/3167094

Library availability

Discover UIUC Full Text

Cite this

Adapting proof automation to adapt proofs. / Ringer, Talia; Leo, John; Yazdani, Nathaniel et al.
CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. ed. / Amy Felty; June Andronick. Association for Computing Machinery, 2018. p. 115-129.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Ringer, T, Leo, J, Yazdani, N & Grossman, D 2018, Adapting proof automation to adapt proofs. in A Felty & J Andronick (eds), CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. Association for Computing Machinery, pp. 115-129, 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, United States, 1/8/18. https://doi.org/10.1145/3167094

@inproceedings{7c8d65ec9fa844239dcb0071f6aa5d1b,

title = "Adapting proof automation to adapt proofs",

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.",

keywords = "Proof automation, Proof evolution, Proof repair",

author = "Talia Ringer and John Leo and Nathaniel Yazdani and Dan Grossman",

note = "Publisher Copyright: {\textcopyright} 2018 Copyright held by the owner/author(s). Publication rights licensed to the Association for Computing Machinery.; 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 ; Conference date: 08-01-2018 Through 09-01-2018",

year = "2018",

month = jan,

day = "8",

doi = "10.1145/3167094",

language = "English (US)",

pages = "115--129",

editor = "Amy Felty and June Andronick",

booktitle = "CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018",

publisher = "Association for Computing Machinery",

address = "United States",

}

TY - GEN

T1 - Adapting proof automation to adapt proofs

AU - Ringer, Talia

AU - Leo, John

AU - Yazdani, Nathaniel

AU - Grossman, Dan

PY - 2018/1/8

Y1 - 2018/1/8

N2 - 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.

AB - 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.

KW - Proof automation

KW - Proof evolution

KW - Proof repair

UR - http://www.scopus.com/inward/record.url?scp=85044322662&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85044322662&partnerID=8YFLogxK

U2 - 10.1145/3167094

DO - 10.1145/3167094

M3 - Conference contribution

AN - SCOPUS:85044322662

SP - 115

EP - 129

BT - CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018

A2 - Felty, Amy

A2 - Andronick, June

PB - Association for Computing Machinery

T2 - 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018

Y2 - 8 January 2018 through 9 January 2018

ER -

Adapting proof automation to adapt proofs

Abstract

Conference

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this