From: Stefan <stefanzetzsche@gmail.com>
**
** 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
**
** https://popl24.sigplan.org/home/dafny-2024
** https://dafny24.hotcrp.com/
**
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
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
** ORGANISATION
Program Chairs:
Program Committee:
Steering Committee:
** 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/
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>).
Last updated: Jan 04 2025 at 20:18 UTC