(2nd CfP) Dafny Workshop at POPL 24


** Update: Program Committee





** Dafny at POPL 2024

** 1st Workshop on the Dafny Programming and Verification Language

** 14th of January 2024, London, United Kingdom


** Submission Deadline:

** October 11, 2023


** Dafny 2024 - POPL 2024

** https://dafny24.hotcrp.com/



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, …)


  • Submission: Wednesday, October 11, 2023 (AoE)

  • Notification: Wednesday, November 15, 2023

  • Workshop: Sunday, January 14, 2024


Program Chairs:

  • Joseph Tassarotti (New York University)

  • Stefan Zetzsche (Amazon Web Services)

Program Committee:

  • Adam Chlipala (Massachusetts Institute of Technology)

  • Jean-Christophe Filliatre (CNRS)

  • Andrea Lattuada (VMware Research Group)

  • Elaine Li (New York University)

  • Peter Müller (ETH Zurich)

  • Nadia Polikarpova (University of California, San Diego)

Steering Committee:

  • Rustan Leino (Amazon Web Services)

  • Jean-Baptiste Tristan (Amazon Web Services)


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:


We don’t intend to publish the workshop’s submissions. However, presentations

may be recorded and the videos may be made publicly available.


All questions about submission should be emailed to the program chairs Stefan

Zetzsche (stefanze@amazon.com) and Joseph Tassarotti (jt4767@nyu.edu).