Mostly Automated Proof Repair for Verified Libraries

Explore a groundbreaking 19-minute video presentation from the PLDI 2023 conference that introduces a novel approach to automated proof repair for verified libraries. Delve into the challenges of maintaining formally specified and verified software, focusing on the problem of keeping code and correctness proofs synchronized. Discover the first proof repair methodology for higher-order imperative functions initially verified in the Coq proof assistant. Learn about the innovative combination of dynamic program alignment, enumerative invariant synthesis, and proof-driven testing techniques used to efficiently prune the space of invariant candidates. Examine the implementation of this approach in the Sisyphus tool, which automates the proof repair process for OCaml functions verified in Coq. Gain insights into the tool's evaluation on 10 OCaml programs from popular libraries, demonstrating its ability to repair proofs and suggest correct invariants. Access supplementary materials, including the article, archive, and web page, to further explore this significant advancement in automated proof repair for verified software.