Dafny 2024

Overview

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:

https://dafny24.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) and Joseph Tassarotti (jt4767@nyu.edu).