[TYPES/announce] (2nd CfP) Dafny Workshop at POPL 2025

[Stefan Zetzsche]

-----------------------------------------------------------------------------------------------------------------------------------
**
**    Update: Program Committee, Keynote
**
-----------------------------------------------------------------------------------------------------------------------------------
**
**    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
**
**    Submission Deadline:
**    October 16, 2024
**
**    https://urldefense.com/v3/__https://popl25.sigplan.org/home/dafny-2025__;!!IBzWLUs!RMRzatbJrNFEEciyvhAYTI1FBl1u_PZD3dphGUgdJXdtSisLPuNqfvssnZ0nK_kVOJDB72kwgCnexCFT7AS4dGTntKMSZqLbb5bxNfA$ 
**    https://urldefense.com/v3/__https://dafny25.hotcrp.com__;!!IBzWLUs!RMRzatbJrNFEEciyvhAYTI1FBl1u_PZD3dphGUgdJXdtSisLPuNqfvssnZ0nK_kVOJDB72kwgCnexCFT7AS4dGTntKMSZqLbGPNNqcI$ 
**
-----------------------------------------------------------------------------------------------------------------------------------

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 16, 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://urldefense.com/v3/__https://dafny25.hotcrp.com__;!!IBzWLUs!RMRzatbJrNFEEciyvhAYTI1FBl1u_PZD3dphGUgdJXdtSisLPuNqfvssnZ0nK_kVOJDB72kwgCnexCFT7AS4dGTntKMSZqLbGPNNqcI$ 

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

https://urldefense.com/v3/__https://www.sigplan.org/Resources/Author/__;!!IBzWLUs!RMRzatbJrNFEEciyvhAYTI1FBl1u_PZD3dphGUgdJXdtSisLPuNqfvssnZ0nK_kVOJDB72kwgCnexCFT7AS4dGTntKMSZqLbzXPAExI$ 

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 at amazon.com).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20240916/6e738c48/attachment-0001.htm>