----------------------------------------------------------------------------------------------------------
**
** Update: Program Committee
**
----------------------------------------------------------------------------------------------------------
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:
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).