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

[Stefan Zetzsche]

-----------------------------------------------------------------------------------------------------------------------------------
**
**    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!WL90-etAcrpLGOA2zM_Fy8Z9ltTATFw8L6GEOYTunMp8WOPQtoKMpP1XebyNAbCtQiVgIKzgrF_tUMe9JuQKgPwMmX9tbnXmVXJf3e4$ 
**    https://urldefense.com/v3/__https://dafny25.hotcrp.com__;!!IBzWLUs!WL90-etAcrpLGOA2zM_Fy8Z9ltTATFw8L6GEOYTunMp8WOPQtoKMpP1XebyNAbCtQiVgIKzgrF_tUMe9JuQKgPwMmX9tbnXmdD31r9s$ 
**
-----------------------------------------------------------------------------------------------------------------------------------

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!WL90-etAcrpLGOA2zM_Fy8Z9ltTATFw8L6GEOYTunMp8WOPQtoKMpP1XebyNAbCtQiVgIKzgrF_tUMe9JuQKgPwMmX9tbnXmdD31r9s$ 

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!WL90-etAcrpLGOA2zM_Fy8Z9ltTATFw8L6GEOYTunMp8WOPQtoKMpP1XebyNAbCtQiVgIKzgrF_tUMe9JuQKgPwMmX9tbnXmBO_8nWI$ 

We don’t intend to publish the workshop’s submissions. However,
presentations may be
recorded and the videos may be made publicly available.

-----------------------------------------------------------------------------------------------------------------------------------
** ORGANISATION
-----------------------------------------------------------------------------------------------------------------------------------

Program Chairs:
- Stefan Zetzsche (Amazon Web Services)

Steering Committee:
- 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/20240822/0d1d485e/attachment.htm>