Dafny 2026

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

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:

https://dafny26.hotcrp.com

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).

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.