@inproceedings{cho2024a,
author = {Cho, Chanhee and Zhou, Yi and Bosamiya, Jay and Parno, Bryan},
title = {A Framework for Debugging Automated Program Verification Proofs via Proof Actions},
booktitle = {International Conference on Computer Aided Verification (CAV)},
year = {2024},
month = {July},
abstract = {Many program verification tools provide automation via SMT solvers, allowing them to automatically discharge many proofs. However, when a proof fails, it can be hard to understand why it failed or how to fix it. The main feedback the developer receives is simply the verification result (i.e., success or failure), with no visibility into the solver's internal state. To assist developers using such tools, we introduce ProofPlumber, a novel and extensible proof-action framework for understanding and debugging proof failures. Proof actions act on the developer's source-level proofs (e.g., assertions and lemmas) to determine why they failed and potentially suggest remedies. We evaluate ProofPlumber by writing a collection of proof actions that capture common proof debugging practices. We produce 17 proof actions, each only 29–176 lines of code.},
url = {http://approjects.co.za/?big=en-us/research/publication/a-framework-for-debugging-automated-program-verification-proofs-via-proof-actions/},
}