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
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 16, 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:
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).
| Wed 16 Oct 2024 Submission |
| Wed 20 Nov 2024 Notification |
| Sun 19 Jan 2025 Workshop |
