CMU research team wins CAV 2024 Distinguished Paper Award

A team of Carnegie Mellon University researchers has received the 36th International Conference on Computer Aided Verification (CAV) Distinguished Paper Award for the tool paper A Framework for Debugging Automated Program Verification Proofs via Proof Actions.

The team features CMU Ph.D. students Chanhee Cho and Yi Zhou; recent Ph.D. alumnus Jay Bosamiya; and Bryan Parno, Kavčić-Moura professor of Electrical and Computer Engineering and Computer Science.

“It’s wonderful to receive this acknowledgement of all of the hard work that the students, especially lead author Chanhee Cho, put into this project,” said Parno.

The award was presented to the team by Program Chairs Arie Gurnkel and Vijay Ganesh on Wednesday, July 24 at the CAV 2024 Reception at Concordia University in Montreal.

Program verification allows developers to mathematically prove their code will be correct, reliable, and/or secure. Many verification tools rely on an underlying solver to automatically discharge large parts of the necessary proofs. However, when the solver fails to complete a proof, it can be difficult for developers to understand why it failed or how to fix the proof.

In this paper, the researchers 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 to determine why they failed and to potentially suggest remedies.

“We’re hopeful that ProofPlumber will make it easier to write verified software, and hence give us greater confidence in our digital infrastructure,” said Parno.

CAV is the top conference on computer-aided verification. It focuses on work that uses automation to help designers build better, more reliable systems.