POPL 2024
Wed 17 - Fri 19 January 2024 London, United Kingdom


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 provide a platform for reports about applications of Dafny in industry, research on programming-language concepts that are relevant to Dafny, and talks about Dafny’s role in teaching. Topics include but are not limited to the following:

  • Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and under-approximation, …
  • Interactive theorem proving and SMT automation
  • Coinduction and corecursion
  • Dynamic frames vs. separation logic vs. ownership
  • Test generation for Dafny
  • Specification and proof inference for Dafny
  • Extensions and applications of Dafny
  • Alternative verifier backends
  • Program verification at industry-scale
  • Translation to or from Dafny and other languages
  • Logical foundations for Dafny (partial functions, nonempty types, extreme predicates, …)
  • Dafny in teaching
  • Comparison with other auto-active program verifiers (SPARK, F*, Why3, Viper, Whiley, …)
  • Comparison with other proof assistants (Coq, Isabelle/HOL, Lean, …)

Call for Papers

We don’t intend to publish the workshop’s submissions. However, presentations may be recorded and the videos may be made publicly available.

Important Dates

  • Submission: Wednesday, October 11, 2023 (AoE)
  • Notification: Wednesday, November 15, 2023
  • Workshop: Sunday, January 14, 2024

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:



All questions about submission should be emailed to the program chairs Stefan Zetzsche (stefanze@amazon.com) and Joseph Tassarotti (jt4767@nyu.edu).

Questions? Use the Dafny contact form.