About
There is an established group of verification-aware programming languages that have native support for specifications and proofs, and are equipped with an auto-active static program verifier. Examples of such languages are Dafny, SPARK, F*, Why3, Viper, Whiley. Auto-active tools also exist for other languages like C, Java or Rust. The workshop aims to be a forum for all auto-active program verifiers and their related techniques.
Topics include but are not limited to the following:
- AI for verification and vice versa
- Alternative verifier backends
- Coinduction and corecursion
- Comparison with interactive proof assistants (Rocq, Isabelle/HOL, Lean, …)
- Dynamic frames vs. separation logic vs. ownership
- Extensions and applications of the auto-active language
- GUI and IDE for auto-active verification
- User interaction features
- Logical foundations (partial functions, nonempty types, extreme predicates, …)
- Program verification at industry-scale
- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and under-approximation, …
- SMT automation
- Specification and proof inference for the auto-active language
- Test generation
- Translation to or from the auto-active language
- Verification in teaching
This program is tentative and subject to change.
Sun 11 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 12mDay opening | Day opening Dafny | ||
09:12 60mKeynote | Software Verification meets Real-World Cryptography Dafny Karthikeyan Bhargavan Cryspen, France | ||
10:12 18mTalk | The Design of an Interactive Proof Mode for Dafny Dafny Ștefan Ciobâcă Alexandru Ioan Cuza University of Iasi, K. Rustan M. Leino Amazon, Ștefan Mercaș Alexandru Ioan Cuza University, Iasi, Romania, Roxana-Mihaela Timon Alexandru Ioan Cuza University, Iasi, Romania | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break POPL Catering | ||
11:00 - 12:30 | |||
11:00 18mTalk | Diagnostics in Probabilistic Program Verification Dafny Philipp Schröer RWTH Aachen University, Darion Haase RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University | ||
11:18 18mTalk | Explicit Abstraction Barrier for Autoactive Verification Dafny Paul Patault Université Paris-Saclay - Laboratoire de Méthodes Formelles Pre-print | ||
11:36 18mTalk | Managing the Proof Context in SPARK Dafny | ||
11:54 18mTalk | Tunable Automation in Automated Program Verification Dafny Alexander Bai New York University, Chris Hawblitzel Microsoft Research, Andrea Lattuada VMware Research | ||
12:12 18mTalk | Velvet: A Multi-Modal Verifier for Effectful Programs Dafny Vladimir Gladshtein , George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore, Vitaly Kurin Neapolis University Pafos, Ilya Sergey National University of Singapore Pre-print | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch POPL Catering | ||
14:00 - 15:30 | |||
14:00 18mTalk | Lessons from Building an Auto-Active Verifier in Lean Dafny George Pîrlea National University of Singapore, Vladimir Gladshtein , Qiyuan Zhao National University of Singapore, Ilya Sergey National University of Singapore Pre-print | ||
14:18 18mTalk | Formal Verification of Minimax Algorithms Dafny Wieger Wesselink Eindhoven University of Technology, Kees Huizing Eindhoven University of Technology, Huub van de Wetering Eindhoven University of Technology File Attached | ||
14:36 18mTalk | Teaching Automata Theory and Formal Languages with Dafny Dafny Ran Ettinger NVIDIA and Ben-Gurion University of the Negev and Israel Academic College in Ramat Gan | ||
14:54 18mTalk | Verification of E-Voting Algorithms in Dafny Dafny Robert Büttner University of Regensburg, Fabian Franz Dießl University of Regensburg, Patrick Janoschek University of Regensburg, Ivana Kostadinovic University of Regensburg, Henrik Oback University of Regensburg, Kilian Voß University of Regensburg, Franziska Alber University of Regensburg, Roland Herrmann University of Regensburg, Sibylle Möhle University of Regensburg, Philipp Rümmer University of Regensburg and Uppsala University | ||
15:12 18mTalk | A Correct-by-Construction Checker for Validation of Railway Data Dafny Benoît Boyer Mitsubishi Electric R&D Centre Europe, Rennes, France, Noé Canva Inria Saclay & Université Paris-Saclay, Matteo Manighetti IRIF, Université Paris Cité, Claude Marché Inria Saclay & Université Paris-Saclay | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break POPL Catering | ||
16:00 - 18:00 | |||
16:00 18mTalk | 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 18mTalk | 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 18mTalk | DafnyPro: LLM-Assisted Automated Verification for Dafny Programs Dafny | ||
16:54 18mTalk | 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 18mTalk | 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 INESC TEC, Faculdade de Engenharia, Universidade do Porto | ||
17:30 18mTalk | 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 | ||
17:48 12mDay closing | Day closing Dafny | ||
Accepted Papers
Call for Papers
The workshop won’t have formal proceedings. However, presentations may be recorded and the videos may be made publicly available. You are free to submit work for presentation that is or will be published elsewhere.
Important Dates
Submission: Wednesday, October 22, 2025 (AoE)
Notification: Wednesday, November 12, 2025 (AoE)
Workshop: Sunday, January 11, 2026
Submission Guidelines
To give a presentation at the workshop, please submit an anonymous extended abstract (2-6 pages, excluding references) via hotcrp:
Please use the acmart two-column sigplan sub-format LaTeX style to prepare your submission:
https://www.sigplan.org/Resources/Author/
Authors may additionally submit an anonymised artifact, either by uploading it directly via hotcrp or hosting it on e.g. Zenodo and referring to it on hotcrp. Typically, artifacts are submitted either as tarballs with build instructions, or, ideally, as Docker/VM images.
Contact
All questions about submission should be emailed to the program chairs Stefan Zetzsche (stefanze@amazon.com) or Yannick Moy (yannick.moy@gmail.com).
Keynote
Speaker: Karthikeyan Bhargavan
Title: Software Verification meets Real-World Cryptography
Abstract: In recent years, several software verification frameworks have been applied to analyze the correctness and security of implementations of cryptographic algorithms and protocols, with some notable successes. I will describe what makes the analysis of real-world cryptography interesting and challenging for formal verification, using examples from several research and commercial projects I have participated in. We will discuss the limits of what can be proved today, what remains to be done, and what challenges I see on the horizon.
| Sun 11 Jan 2026 Workshop |
| Wed 12 Nov 2025 Notification |
| Wed 22 Oct 2025 Submission |
