<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;"><div class="WordSection1" style="page: WordSection1;"><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;">** Update: Program Committee<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;">** 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!VFiMwMp5rhCkosZZbbUkKafoTRfj7x172gw-03-dSI0xRM4w1O2Z5IzjGs0uytPvqdLhitK8Imlpe6JcEM2Tb4-q2VdNDsrnhaqTtzE$" 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!VFiMwMp5rhCkosZZbbUkKafoTRfj7x172gw-03-dSI0xRM4w1O2Z5IzjGs0uytPvqdLhitK8Imlpe6JcEM2Tb4-q2VdNDsrngE_C_V0$" 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;"><br></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;">** ORGANISATION<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;">Program Chairs:<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Joseph Tassarotti (New York University)<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Stefan Zetzsche (Amazon Web Services)<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;">Program Committee:<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Adam Chlipala (Massachusetts Institute of Technology)<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Jean-Christophe Filliatre (CNRS)<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Andrea Lattuada (VMware Research Group)<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Elaine Li (New York University)<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Peter Müller (ETH Zurich)<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Nadia Polikarpova (University of California, San Diego)<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;">Steering Committee:<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Rustan Leino (Amazon Web Services)<o:p></o:p></p><p class="MsoNormal" style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;">- Jean-Baptiste Tristan (Amazon Web Services)<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!VFiMwMp5rhCkosZZbbUkKafoTRfj7x172gw-03-dSI0xRM4w1O2Z5IzjGs0uytPvqdLhitK8Imlpe6JcEM2Tb4-q2VdNDsrngmV4sRg$">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!VFiMwMp5rhCkosZZbbUkKafoTRfj7x172gw-03-dSI0xRM4w1O2Z5IzjGs0uytPvqdLhitK8Imlpe6JcEM2Tb4-q2VdNDsrn3WwFFm4$">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>).<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;"><br></p></div></body></html>