POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

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:

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

Questions? Use the Dafny contact form.