POPL 2025 (series) / Dafny 2025 (series) / Dafny 2025 /
DafnyBench: A Benchmark for Formal Software Verification
This program is tentative and subject to change.
Sun 19 Jan 2025 17:12 - 17:30 at Hopscotch - Verified Code Synthesis
We introduce DafnyBench, the largest benchmark of its kind for training and evaluating machine learning systems for formal software verification. We test the ability of LLMs such as GPT-4 and Claude 3 to auto-generate enough annotations for the Dafny formal verification engine to successfully verify over 750 programs with about 53,000 lines of code. The best model and prompting scheme achieved 68% success rate, and we quantify how this rate improves when retrying with error message feedback and how it deteriorates with the amount of required code and annotations. We hope that DafnyBench will enable rapid improvements from this baseline as LLMs and verification techniques grow in quality.
This program is tentative and subject to change.
Sun 19 JanDisplayed time zone: Mountain Time (US & Canada) change
Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change
16:00 - 18:00 | |||
16:00 18mTalk | Laurel: Unblocking Automated Verification with Large Language Models Dafny Eric Mugnier University of California San Diego, Emmanuel Anaya Gonzalez UCSD, Nadia Polikarpova University of California at San Diego, Ranjit Jhala University of California at San Diego, Zhou Yuanyuan UCSD | ||
16:18 18mTalk | VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search Dafny David Brandfonbrener Harvard, Simon Henniger Technical University of Munich, Sibi Raja Harvard, Tarun Prasad Harvard, Chloe Loughridge Harvard University, Federico Cassano Northeastern University, Sabrina Ruixin Hu Harvard, Jianang Yang Million.js, William E. Byrd University of Alabama at Birmingham, USA, Robert Zinkov University of Oxford, Nada Amin Harvard University | ||
16:36 18mTalk | dafny-annotator: AI-Assisted Verification of Dafny Programs Dafny Gabriel Poesia Stanford University, Chloe Loughridge Harvard University, Nada Amin Harvard University | ||
16:54 18mTalk | Dafny as Verification-Aware Intermediate Language for Code Generation Dafny Yue Chen Li Massachusetts Institute of Technology, Stefan Zetzsche Amazon Web Services, Siva Somayyajula Amazon Web Services | ||
17:12 18mTalk | DafnyBench: A Benchmark for Formal Software Verification Dafny Chloe Loughridge Harvard University, Qinyi Sun Massachusetts Institute of Technology, Seth Ahrenbach Beneficial AI Foundation, Federico Cassano Northeastern University, Chuyue Sun Stanford University, Ying Sheng Stanford University, Anish Mudide Massachusetts Institute of Technology, Md Rakib Hossain Misu University of California Irvine, Nada Amin Harvard University, Max Tegmark Massachusetts Institute of Technology | ||
17:30 18mTalk | Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming Dafny Saikat Chakraborty Microsoft Research, Gabriel Ebner Microsoft Research, Siddharth Bhat University of Cambridge, Sarah Fakhoury Microsoft Research, Sakina Fatima University of Ottawa, Shuvendu K. Lahiri Microsoft Research, Nikhil Swamy Microsoft Research | ||
17:48 12mDay closing | Day closing Dafny Stefan Zetzsche Amazon Web Services | ||