<div dir="ltr">-----------------------------------------------------------------------------------------------------------------------------------<br>**<br>**    CALL FOR EXTENDED ABSTRACTS<br>**<br>**    Dafny at POPL 2025<br>**    2nd Workshop on the Dafny Programming and Verification Language<br>**    19th of January 2025, Denver, Colorado, United States<br>**<br>**    Submission Deadline:<br>**    October 16, 2024<br>**<br>**    <a href="https://urldefense.com/v3/__https://popl25.sigplan.org/home/dafny-2025__;!!IBzWLUs!WL90-etAcrpLGOA2zM_Fy8Z9ltTATFw8L6GEOYTunMp8WOPQtoKMpP1XebyNAbCtQiVgIKzgrF_tUMe9JuQKgPwMmX9tbnXmVXJf3e4$">https://popl25.sigplan.org/home/dafny-2025</a><br>**    <a href="https://urldefense.com/v3/__https://dafny25.hotcrp.com__;!!IBzWLUs!WL90-etAcrpLGOA2zM_Fy8Z9ltTATFw8L6GEOYTunMp8WOPQtoKMpP1XebyNAbCtQiVgIKzgrF_tUMe9JuQKgPwMmX9tbnXmdD31r9s$">https://dafny25.hotcrp.com</a><br>**<br>-----------------------------------------------------------------------------------------------------------------------------------<br><div><br>Dafny is a verification-aware programming language that has native support for specifications </div><div>and proofs, and is equipped with an auto-active static program verifier. The workshop aims to </div><div>provide a platform for reports about applications of Dafny in industry, research on programming-</div><div>language concepts that are relevant to Dafny, and talks about Dafny’s role in teaching. Topics<br>include but are not limited to the following:</div><div><br></div><div>- Alternative verifier backends<br>- Coinduction and corecursion<br>- Comparison with other auto-active program verifiers (SPARK, F*, Why3, Viper, Whiley, …)<br>- Comparison with other proof assistants (Coq, Isabelle/HOL, Lean, …)<br>- Dafny in teaching<br>- Dynamic frames vs. separation logic vs. ownership<br>- Extensions and applications of Dafny<br>- Interactive theorem proving and SMT automation<br>- Logical foundations for Dafny (partial functions, nonempty types, extreme predicates, …)<br>- Program verification at industry-scale<br>- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and under-approximation, …<br>- Specification and proof inference for Dafny<br>- Test generation for Dafny<br>- Translation to or from Dafny and other languages<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** IMPORTANT DATES<br>-----------------------------------------------------------------------------------------------------------------------------------<div><br>- Submission: Wednesday, October 16, 2024 (AoE)<br>- Notification: Wednesday, November 20, 2024<br>- Workshop: Sunday, January 19, 2025<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** SUBMISSION GUIDELINES<br>-----------------------------------------------------------------------------------------------------------------------------------</div><div><br>To give a presentation at the workshop, please submit an anonymous extended abstract </div><div>(2-6 pages, excluding references) via hotcrp:</div><div><br><a href="https://urldefense.com/v3/__https://dafny25.hotcrp.com__;!!IBzWLUs!WL90-etAcrpLGOA2zM_Fy8Z9ltTATFw8L6GEOYTunMp8WOPQtoKMpP1XebyNAbCtQiVgIKzgrF_tUMe9JuQKgPwMmX9tbnXmdD31r9s$">https://dafny25.hotcrp.com</a><br><br>Please use the acmart two-column sigplan sub-format LaTeX style to prepare<br>your submission:<br><br><a href="https://urldefense.com/v3/__https://www.sigplan.org/Resources/Author/__;!!IBzWLUs!WL90-etAcrpLGOA2zM_Fy8Z9ltTATFw8L6GEOYTunMp8WOPQtoKMpP1XebyNAbCtQiVgIKzgrF_tUMe9JuQKgPwMmX9tbnXmBO_8nWI$">https://www.sigplan.org/Resources/Author/</a><br><br>We don’t intend to publish the workshop’s submissions. However, presentations may be </div><div>recorded and the videos may be made publicly available.</div><div><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** ORGANISATION<br>-----------------------------------------------------------------------------------------------------------------------------------</div><div><br>Program Chairs:<br>- Stefan Zetzsche (Amazon Web Services)<br> <br>Steering Committee:<br>- Rustan Leino (Amazon Web Services)<br>- Joseph Tassarotti (New York University)<br>- Jean-Baptiste Tristan (Amazon Web Services)<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** CONTACT<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br></div><div>All questions about submission should be emailed to the program chair Stefan Zetzsche </div><div>(<a href="mailto:stefanze@amazon.com">stefanze@amazon.com</a>).</div><div><br></div></div></div>