Workshop on Dafny at POPL 24 (Call for Papers)

----------------------------------------------------------------------------------------------------------

**

**    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 ([email protected]) and Joseph Tassarotti ([email protected]).