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

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

Accepted Papers

Title
Caesar: A Verifier for Probabilistic Programs
Dafny
CLOVER: Closed-Loop Verifiable Code Generation
Dafny
Colouring Flags with Dafny & Idris
Dafny
Dafny Test Generation
Dafny
Domesticating Automation
Dafny
Enhancing Proof Stability
Dafny
Generation of Verified Assembly Code Using Dafny and Reinforcement Learning
Dafny
Improving the Stability of Type Safety Proofs in Dafny
Dafny
Incremental Proof Development in Dafny with Module-Based Induction
Dafny
Learn 'em Dafny
Dafny
Portfolio Solving for Dafny
Dafny
Randomised Testing of the Dafny Compiler
Dafny
Teaching Logic and Set Theory with Dafny
Dafny
Testing Specifications In Dafny
Dafny
Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
Dafny
Verifying Dafny Contract Integrity
Dafny
VMC: a Dafny Library for Verified Monte Carlo Algorithms
Dafny

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 18 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).

Questions? Use the Dafny contact form.