Dafny 2025

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 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:

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

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 16 30, 2024 (AoE)

Notification: Wednesday, November 20, 2024

Workshop: Sunday, January 19, 2025

Submission Guidelines

To give a presentation at the workshop, please submit an anonymous extended abstract (2-6 pages, excluding references) via hotcrp:

https://dafny25.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 chair Stefan Zetzsche (stefanze@amazon.com).