ASE 2024
Sun 27 October - Fri 1 November 2024 Sacramento, California, United States
Wed 30 Oct 2024 13:45 - 14:00 at Carr - Verification Chair(s): Tevfik Bultan

We investigate a modification of the classical Bounded Model Checking (BMC) procedure that does not handle loops through unrolling but via modifications to the control flow graph (CFG). A portion of the CFG representing a loop is replaced by a node asserting invariants of the loop. We generate these invariants using Large Language Models (LLMs) and use a first-order theorem prover to ensure the correctness of the generated statements. We thus transform programs to loop-free variants in a sound manner. Our experimental results show that the resulting tool, \ourtool{}, is competitive with state-of-the-art formal verifiers for programs with unbounded loops, significantly improving the number of programs verified by the industrial-strength software verifier ESBMC and verifying programs that state-of-the-art software verifiers such as SeaHorn and VeriAbs could not.

Wed 30 Oct

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 15:00
VerificationResearch Papers / Tool Demonstrations at Carr
Chair(s): Tevfik Bultan University of California at Santa Barbara
13:30
15m
Talk
LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant InferenceACM SigSoft Distinguished Paper Award
Research Papers
Guangyuan Wu Nanjing University, Weining Cao Nanjing University, Yuan Yao Nanjing University, Hengfeng Wei State Key Laboratory for Novel Software Technology, Nanjing University, Taolue Chen Birkbeck, University of London, Xiaoxing Ma State Key Laboratory for Novel Software Technology, Nanjing University
13:45
15m
Talk
LLM-Generated Invariants for Bounded Model Checking Without Loop UnrollingACM SigSoft Distinguished Paper Award
Research Papers
Muhammad A. A. Pirzada The University of Manchester, Giles Reger University of Manchester, Ahmed Bhayat Independent Scholar, Lucas C. Cordeiro University of Manchester, UK and Federal University of Amazonas, Brazil
Link to publication DOI
14:00
15m
Talk
Proof Automation with Large Language Models
Research Papers
Minghai Lu Purdue University, Benjamin Delaware Purdue University, Tianyi Zhang Purdue University
Pre-print
14:15
15m
Talk
Verifying the Option Type With Rely-Guarantee Reasoning
Research Papers
James Yoo University of Washington, Michael D. Ernst University of Washington, René Just University of Washington
Link to publication DOI
14:30
10m
Talk
CoVeriTeam GUI: A No-Code Approach to Cooperative Software Verification
Tool Demonstrations
Thomas Lemberger LMU Munich, Henrik Wachowitz LMU Munich
14:40
10m
Talk
CoqPilot, a plugin for LLM-based generation of proofs
Tool Demonstrations
Andrei Kozyrev JetBrains Research, Constructor University Bremen, Gleb Solovev JetBrains Research, Constructor University Bremen, Nikita Khramov JetBrains Research, Constructor University Bremen, Anton Podkopaev JetBrains Research, Constructor University