<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">----------------------------------------------------------------------------------------------------------<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">**<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">** CALL FOR EXTENDED ABSTRACTS<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">**<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">** Dafny at POPL 2024<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">** 1st Workshop on the Dafny Programming and Verification Language<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">** 14th of January 2024, London, United Kingdom<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">**<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">** Submission Deadline:<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">** October 11, 2023<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">**<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">** <span class="apple-converted-space"> </span><a href="https://urldefense.com/v3/__https://popl24.sigplan.org/home/dafny-2024__;!!IBzWLUs!XnBuhDPfO8iySlXlAxucYqWgcjFRiJ_AvcL3Stts4ZwdbxSsiseiJcwVuw7kob8ZhtTPk0zkjmpQK9iWBpSLp5EUNntydBtHcogq9Dk$" title="https://popl24.sigplan.org/home/dafny-2024" style="color: rgb(5, 99, 193);">https://popl24.sigplan.org/home/dafny-2024</a><o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">** <span class="apple-converted-space"> </span><a href="https://urldefense.com/v3/__https://dafny24.hotcrp.com/__;!!IBzWLUs!XnBuhDPfO8iySlXlAxucYqWgcjFRiJ_AvcL3Stts4ZwdbxSsiseiJcwVuw7kob8ZhtTPk0zkjmpQK9iWBpSLp5EUNntydBtHdAhaGBI$" title="https://dafny24.hotcrp.com/" style="color: rgb(5, 99, 193);">https://dafny24.hotcrp.com/</a><o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">**<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">-----------------------------------------------------------------------------------------------------------<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><o:p> </o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">* OVERVIEW<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><o:p> </o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">Dafny is a verification-aware programming language that has native support<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">for specifications and proofs, and is equipped with an auto-active static<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">program verifier. The workshop aims to provide a platform for reports about<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">applications of Dafny in industry, research on programming-language concepts<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">that are relevant to Dafny, and talks about Dafny’s role in teaching. Topics<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">include but are not limited to the following:<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><o:p> </o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"> under-approximation, ...<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Interactive theorem proving and SMT automation<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Coinduction and corecursion<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Dynamic frames vs. separation logic vs. ownership<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Test generation for Dafny<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Specification and proof inference for Dafny<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Extensions and applications of Dafny<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Alternative verifier backends<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Program verification at industry-scale<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Translation to or from Dafny and other languages<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Logical foundations for Dafny (partial functions, nonempty types, extreme<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"> predicates, ...)<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Dafny in teaching<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Comparison with other auto-active program verifiers (SPARK, F*, Why3,<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"> Viper, Whiley, ...)<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Comparison with other proof assistants (Coq, Isabelle/HOL, Lean, ...)<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><o:p> </o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">-----------------------------------------------------------------------------------------------------------<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">** IMPORTANT DATES<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">-----------------------------------------------------------------------------------------------------------<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><o:p> </o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Submission: Wednesday, October 11, 2023 (AoE)<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Notification: Wednesday, November 15, 2023<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Workshop: Sunday, January 14, 2024<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><o:p> </o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">-----------------------------------------------------------------------------------------------------------<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">** SUBMISSION GUIDELINES<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">-----------------------------------------------------------------------------------------------------------<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><o:p> </o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">To give a presentation at the workshop, please submit an anonymous extended<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">abstract (2-6 pages, excluding references) via hotcrp:<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><br></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><font color="#0563c1"><a href="https://urldefense.com/v3/__https://dafny24.hotcrp.com/__;!!IBzWLUs!XnBuhDPfO8iySlXlAxucYqWgcjFRiJ_AvcL3Stts4ZwdbxSsiseiJcwVuw7kob8ZhtTPk0zkjmpQK9iWBpSLp5EUNntydBtHdAhaGBI$">https://dafny24.hotcrp.com</a></font><o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><br></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">Please use the acmart two-column sigplan sub-format LaTeX style to prepare<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">your submission:<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><br></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><font color="#0563c1"><a href="https://urldefense.com/v3/__https://www.sigplan.org/Resources/Author/__;!!IBzWLUs!XnBuhDPfO8iySlXlAxucYqWgcjFRiJ_AvcL3Stts4ZwdbxSsiseiJcwVuw7kob8ZhtTPk0zkjmpQK9iWBpSLp5EUNntydBtHzcFBSfY$">https://www.sigplan.org/Resources/Author/</a></font><o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><br></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">We don’t intend to publish the workshop’s submissions. However, presentations<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">may be recorded and the videos may be made publicly available.<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><o:p> </o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">-----------------------------------------------------------------------------------------------------------<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">** CONTACT<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">-----------------------------------------------------------------------------------------------------------<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><o:p> </o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">All questions about submission should be emailed to the program chairs Stefan<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">Zetzsche (<a href="mailto:stefanze@amazon.com" title="mailto:stefanze@amazon.com" style="color: rgb(5, 99, 193);">stefanze@amazon.com</a>) and Joseph Tassarotti (<a href="mailto:jt4767@nyu.edu" title="mailto:jt4767@nyu.edu" style="color: rgb(5, 99, 193);">jt4767@nyu.edu</a>).</p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;"><br></p></body></html>