Workshop on Dafny at POPL 24

Announcements
1

**

** CALL FOR EXTENDED ABSTRACTS

**

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

**

** https://popl24.sigplan.org/home/dafny-2024

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

**

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

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

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

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

** CONTACT

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

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