Proof Maintenance for Certified Libraries
27/01/2023, 3pm
Speaker
Abstract
The cost of maintaining formally specified and verified software is widely considered prohibitively high due to the need to constantly keep code and the proofs of its correctness in sync—the problem known as proof repair. One of the main challenges in automated proof repair for evolving code is to infer invariants for a new version of a once verified program that are strong enough to establish its full functional correctness. In this work, we present the first proof repair methodology for higher-order imperative functions, whose initial versions were verified in the Coq proof assistant and whose specifications remained unchanged. We recast the automated invariant inference problem as a repair task: new invariant candidates are derived from facts about the old version of the program. Our proof repair procedure is based on the combination of dynamic program alignment, enumerative invariant synthesis, and a novel technique for efficiently pruning the space of invariant candidates, dubbed proof-driven testing, enabled by the constructive nature of Coq’s proof certificates. We have implemented our approach in a mostly-automated proof repair tool.
Bio
Kiran Gopinathan is a fourth year PhD student working with Ilya Sergey at NUS. His work investigates the design and development of meta-tooling for formal verification, such as automatically synthesizing or repairing proof scripts for interactive theorem provers.