Adapting proof automation to adapt proofs
Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman · 2018
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.