<div dir="ltr">-----------------------------------------------------------------------------------------------------------------------------------<br>**<br>**    Update: Extended submission deadline<br>**<br>-----------------------------------------------------------------------------------------------------------------------------------<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>**    Extended Submission Deadline:<br>**    October 30, 2024<br>**<br>**    <a href="https://urldefense.com/v3/__https://popl25.sigplan.org/home/dafny-2025__;!!IBzWLUs!TzCT3WCjKtdkSaaj43kVGh7ZnNtaI7dkGMFY-cnS-45eACWMtukqX9y4vImtORpDbWe_G5jX5nHeCcTdULMza-9EwzOvEdGjOSNQLY8$" target="_blank">https://popl25.sigplan.org/home/dafny-2025</a><br>**    <a href="https://urldefense.com/v3/__https://dafny25.hotcrp.com/__;!!IBzWLUs!TzCT3WCjKtdkSaaj43kVGh7ZnNtaI7dkGMFY-cnS-45eACWMtukqX9y4vImtORpDbWe_G5jX5nHeCcTdULMza-9EwzOvEdGjAxrMWsY$" target="_blank">https://dafny25.hotcrp.com</a><br>**<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>Dafny is a verification-aware programming language that has native support for specifications<br>and proofs, and is equipped with an auto-active static program verifier. The workshop aims to<br>provide a platform for reports about applications of Dafny in industry, research on programming-<br>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:<br><br>- 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>-----------------------------------------------------------------------------------------------------------------------------------<br><br>- Submission: Wednesday, October 30, 2024 (AoE)<br>- Notification: Wednesday, November 20, 2024<br>- Workshop: Sunday, January 19, 2025<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** SUBMISSION GUIDELINES<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>To give a presentation at the workshop, please submit an anonymous extended abstract<br>(2-6 pages, excluding references) via hotcrp:<br><br><a href="https://urldefense.com/v3/__https://dafny25.hotcrp.com/__;!!IBzWLUs!TzCT3WCjKtdkSaaj43kVGh7ZnNtaI7dkGMFY-cnS-45eACWMtukqX9y4vImtORpDbWe_G5jX5nHeCcTdULMza-9EwzOvEdGjAxrMWsY$" target="_blank">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!TzCT3WCjKtdkSaaj43kVGh7ZnNtaI7dkGMFY-cnS-45eACWMtukqX9y4vImtORpDbWe_G5jX5nHeCcTdULMza-9EwzOvEdGj0TgT85c$" target="_blank">https://www.sigplan.org/Resources/Author/</a><br><br>The workshop won’t have formal proceedings. However, presentations may be recorded and the <div>videos may be made publicly available. You are free to submit work for presentation that is or will </div><div>be published elsewhere.<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** KEYNOTE<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>Nada Amin (Harvard University)<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** ORGANISATION<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>Program Committee Chairs:<br>- Stefan Zetzsche (Amazon Web Services)<br><br>Program Committee:<br>- Seth Ahrenbach (Beneficial AI Foundation)<br>- Tej Chajed (University of Wisconsin–Madison)<br>- Alastair F. Donaldson (Imperial College London)<br>- Marie Farrell (The University of Manchester)<br>- Bryan Parno (Carnegie Mellon University)<br>- Clément Pit-Claudel (EPFL)<br><br>Steering Committee Chairs:<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>All questions about submission should be emailed to the program chair Stefan Zetzsche<br>(<a href="mailto:stefanze@amazon.com" target="_blank">stefanze@amazon.com</a>).</div></div>