About
Dafny is a verification-aware programming language that has native support for specifications and proofs, and is equipped with an auto-active static program verifier. 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 (Coq, Isabelle/HOL, Lean, …)
- Dynamic frames vs. separation logic vs. ownership
- Extensions and applications of Dafny (or other auto-active verifiers)
- Logical foundations (partial functions, nonempty types, extreme predicates, …)
- Other auto-active program verifiers (SPARK, F, Why3, Viper, Whiley, …)
- Program verification at industry-scale
- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and under-approximation, …
- SMT automation
- Specification and proof inference for Dafny (or other auto-active verifiers)
- Test generation
- Translation to or from Dafny and other languages
- Verification in teaching
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 8, 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/
Contact
All questions about submission should be emailed to the program chairs Stefan Zetzsche (stefanze@amazon.com) or Yannick Moy (yannick.moy@gmail.com).