Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] (2nd CfP) Dafny Workshop at POPL 24

Email Gateway (Sep 27 2023 at 14:26):

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

• 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/

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: Apr 28 2024 at 20:16 UTC