# (2nd CfP) Dafny Workshop at POPL 24

**URL:** <https://discourse.rocq-prover.org/t/2nd-cfp-dafny-workshop-at-popl-24/2056>\
**Category:** Announcements\
**Created:** [September 27, 2023, 2:34pm UTC](https://discourse.rocq-prover.org/t/2nd-cfp-dafny-workshop-at-popl-24/2056 "2023-09-27T14:34:28Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![stefanze](https://avatars.discourse-cdn.com/v4/letter/s/8dc957/32.png) [@stefanze](https://discourse.rocq-prover.org/u/stefanze)\
**Post date:** [September 27, 2023, 2:34pm UTC](https://discourse.rocq-prover.org/t/2nd-cfp-dafny-workshop-at-popl-24/2056/1 "2023-09-27T14:34:28Z")

</div>

* * *

\*\*

\*\* Update: Program Committee

\*\*

* * *

\*\*

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

\*\*

\*\* [Dafny 2024 - POPL 2024](https://popl24.sigplan.org/home/dafny-2024)

\*\* [https://dafny24.hotcrp.com/](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

* * *

\*\* ORGANISATION

* * *

Program Chairs:

- Joseph Tassarotti (New York University)

- Stefan Zetzsche (Amazon Web Services)

Program Committee:

- Adam Chlipala (Massachusetts Institute of Technology)

- Jean-Christophe Filliatre (CNRS)

- Andrea Lattuada (VMware Research Group)

- Elaine Li (New York University)

- Peter Müller (ETH Zurich)

- Nadia Polikarpova (University of California, San Diego)

Steering Committee:

- Rustan Leino (Amazon Web Services)

- Jean-Baptiste Tristan (Amazon Web Services)

* * *

\*\* 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](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/](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](mailto:stefanze@amazon.com)) and Joseph Tassarotti ([jt4767@nyu.edu](mailto:jt4767@nyu.edu)).