4 papers
Programmers Are Poor and Overconfident Judges of LLM-Generated Assertions
Zhanna Kaufman, Yuriy Brun, Adithya Murali +1
Code comprehension and code review are already critically important software engineering tasks, and the rising use of AI code generation tools is only increasing that importance. G…
Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun +3
Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but requires significant effort and expertise. Machine learning can auto…
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
Kyle Thompson, Nuno Saavedra, Pedro Carrott +6
Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual…
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman +3
Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. Recen…