Mon 8 Jan 2018 16:30 - 17:00 at Museum A - Proof Methods and Libraries Chair(s): René Thiemann

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.

Mon 8 Jan

CPP-2018
16:00 - 18:00: CPP 2018 - Proof Methods and Libraries at Museum A
Chair(s): René ThiemannUniversity of Innsbruck
CPP-2018151542360000016:00 - 16:30
Talk
Craig McLaughlinThe University of Edinburgh, James McKinna, Ian StarkThe University of Edinburgh
DOI
CPP-2018151542540000016:30 - 17:00
Talk
Talia RingerUniversity of Washington, Nathaniel YazdaniUniversity of Washington, Seattle, John LeoHalfaya Research, Dan GrossmanUniversity of Washington
DOI
CPP-2018151542720000017:00 - 17:30
Talk
Niklas GrimmVienna University of Technology, Austria, Kenji MaillardInria Paris and ENS Paris, Cédric FournetMicrosoft Research, Cătălin HriţcuInria Paris, Matteo MaffeiSaarland University, Jonathan ProtzenkoMicrosoft Research, n.n., Tahina RamananandroMicrosoft Research, n.n., Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research, Santiago Zanella-BéguelinMicrosoft Research, n.n.
DOI
CPP-2018151542900000017:30 - 18:00
Talk
Hugo FéréeUniversity of Kent, UK, Samuel HymUniversity of Lille, France, Micaela Mayero, Jean-Yves MoyenUniversity of Copenhagen, Denmark, David NowakCNRS, France
DOI