POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Sun 11 Jan 2026 17:30 - 17:48 at Horizons - LLMs in Auto-Active Verification

Recently, Large Language Models (LLMs) have been widely applied to code generation, and recent studies have explored their ability to produce programs in verification languages, including Dafny. Although several benchmarks have been proposed to assess LLM performance in generating Dafny code, existing datasets suffer from several limitations, including no clear verification goals, limited diversity in verification complexity, potential contamination, and heavy reliance on manually collected examples that are publicly available online. In this work, we introduce TACoDafny, an automated pipeline for constructing Dafny verification benchmarks directly from task descriptions sourced from online programming repositories. As a preliminary result, we successfully generated 76 Dafny programs with verifiable properties derived from the task descriptions of the first 200 LeetCode problems. Our pipeline not only enables large-scale benchmark generation, but also facilitates the creation of additional verifiable Dafny code that can be leveraged to train models to further improve their verification capabilities.

Sun 11 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:00 - 18:00
LLMs in Auto-Active VerificationDafny at Horizons
16:00
18m
Talk
ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
Dafny
Mantas Bakšys University of Cambridge, Stefan Zetzsche Amazon Web Services, Olivier Bouissou Amazon Web Services, Soonho Kong Amazon Web Services, Remi Delmas Amazon Web Services
Pre-print
16:18
18m
Talk
A benchmark for vericoding: formally verified program synthesis
Dafny
Sergiu Bursuc Beneficial AI Foundation, Theodore Ehrenborg Beneficial AI Foundation, Shaowei Lin Beneficial AI Foundation, Lăcrămioara Aștefănoaei Beneficial AI Foundation, Ionel Emilian Chiosa MIT, Jure Kukovec Beneficial AI Foundation, Alok Singh Beneficial AI Foundation, Oliver Butterley Beneficial AI Foundation, Adem Bizid MIT, Quinn Dougherty Beneficial AI Foundation, Miranda Zhao MIT, Max Tan MIT, Max Tegmark Massachusetts Institute of Technology
Pre-print File Attached
16:36
18m
Talk
DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
Dafny
Debangshu Banerjee UIUC, Olivier Bouissou Amazon Web Services, Stefan Zetzsche Amazon Web Services
Pre-print
16:54
18m
Talk
MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
Dafny
Mantas Bakšys University of Cambridge, Stefan Zetzsche Amazon Web Services, Olivier Bouissou Amazon Web Services
Pre-print
17:12
18m
Talk
Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
Dafny
Valentina Wu Faculdade de Engenharia, Universidade do Porto, Alexandra Mendes Faculty of Engineering, University of Porto & INESC TEC, Alexandre Abreu University of Porto & INESC TEC
17:30
18m
Talk
Toward Automated, Contamination-free Dafny Benchmark Generation
Dafny
Changjie Wang KTH Royal Institute of Technology, Mariano Scazzariello RISE Research Institutes of Sweden, Dejan Kostic KTH Royal Institute of Technology, Marco Chiesa KTH Royal Institute of Technology
Pre-print
17:48
12m
Day closing
Day closing
Dafny
Stefan Zetzsche Amazon Web Services, Yannick Moy ANSSI