Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Dafny Workshop at POPL 2025 (deadline extension)

Email Gateway (Oct 08 2024 at 22:08):

From: Stefan Zetzsche <stefanzetzsche@gmail.com>

**
** Update: Extended submission deadline
**

**
** CALL FOR EXTENDED ABSTRACTS
**
** Dafny at POPL 2025
** 2nd Workshop on the Dafny Programming and Verification Language
** 19th of January 2025, Denver, Colorado, United States
**
** Extended Submission Deadline:
** October 30, 2024
**
** https://popl25.sigplan.org/home/dafny-2025
** https://dafny25.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:

• Alternative verifier backends
• Coinduction and corecursion

• Comparison with other auto-active program verifiers (SPARK, F*, Why3,
  Viper, Whiley, …)

• Comparison with other proof assistants (Coq, Isabelle/HOL, Lean, …)

• Dafny in teaching
• Dynamic frames vs. separation logic vs. ownership
• Extensions and applications of Dafny
• Interactive theorem proving and SMT automation

• Logical foundations for Dafny (partial functions, nonempty types, extreme
  predicates, …)

• Program verification at industry-scale

• Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and
  under-approximation, …

• Specification and proof inference for Dafny

• Test generation for Dafny
• Translation to or from Dafny and other languages

** IMPORTANT DATES

• Submission: Wednesday, October 30, 2024 (AoE)
• Notification: Wednesday, November 20, 2024
• Workshop: Sunday, January 19, 2025

** SUBMISSION GUIDELINES

To give a presentation at the workshop, please submit an anonymous extended
abstract
(2-6 pages, excluding references) via hotcrp:

https://dafny25.hotcrp.com

Please use the acmart two-column sigplan sub-format LaTeX style to prepare
your submission:

https://www.sigplan.org/Resources/Author/

The workshop won’t have formal proceedings. However, presentations may be
recorded and the
videos may be made publicly available. You are free to submit work for
presentation that is or will
be published elsewhere.

** KEYNOTE

Nada Amin (Harvard University)

** ORGANISATION

Program Committee Chairs:

• Stefan Zetzsche (Amazon Web Services)

Program Committee:

• Seth Ahrenbach (Beneficial AI Foundation)
• Tej Chajed (University of Wisconsin–Madison)
• Alastair F. Donaldson (Imperial College London)
• Marie Farrell (The University of Manchester)
• Bryan Parno (Carnegie Mellon University)
• Clément Pit-Claudel (EPFL)

Steering Committee Chairs:

• Rustan Leino (Amazon Web Services)
• Joseph Tassarotti (New York University)
• Jean-Baptiste Tristan (Amazon Web Services)

** CONTACT

All questions about submission should be emailed to the program chair
Stefan Zetzsche
(stefanze@amazon.com).

Last updated: Jan 04 2025 at 20:18 UTC