<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;">----------------------------------------------------------------------------------------------------------<br>**<br>** Update: Extended Deadline<br>**<br>----------------------------------------------------------------------------------------------------------<br>**<br>** CALL FOR EXTENDED ABSTRACTS<br>**<br>** Dafny at POPL 2024<br>** 1st Workshop on the Dafny Programming and Verification Language<br>** 14th of January 2024, London, United Kingdom<br>**<br>** Submission Deadline:<br>** October 18, 2023<br>**<br>** <a href="https://urldefense.com/v3/__https://popl24.sigplan.org/home/dafny-2024__;!!IBzWLUs!S-gSuH3NQU2QznUp_Jeoxu5kNz5g8YNUhbPKmZ-h2qYF-1gigzoFGvRai2cK4UvhCUrAMhkYSn6n2KnNmm1Gq_8bxoIPmz-I801kb0U$">https://popl24.sigplan.org/home/dafny-2024</a><br>** <a href="https://urldefense.com/v3/__https://dafny24.hotcrp.com/__;!!IBzWLUs!S-gSuH3NQU2QznUp_Jeoxu5kNz5g8YNUhbPKmZ-h2qYF-1gigzoFGvRai2cK4UvhCUrAMhkYSn6n2KnNmm1Gq_8bxoIPmz-I_skQc7A$">https://dafny24.hotcrp.com/</a><br>**<br>-----------------------------------------------------------------------------------------------------------<br><br>* OVERVIEW<br><br>Dafny is a verification-aware programming language that has native support<br>for specifications and proofs, and is equipped with an auto-active static<br>program verifier. The workshop aims to provide a platform for reports about<br>applications of Dafny in industry, research on programming-language concepts<br>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>- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and<br> under-approximation, ...<br>- Interactive theorem proving and SMT automation<br>- Coinduction and corecursion<br>- Dynamic frames vs. separation logic vs. ownership<br>- Test generation for Dafny<br>- Specification and proof inference for Dafny<br>- Extensions and applications of Dafny<br>- Alternative verifier backends<br>- Program verification at industry-scale<br>- Translation to or from Dafny and other languages<br>- Logical foundations for Dafny (partial functions, nonempty types, extreme<br> predicates, ...)<br>- Dafny in teaching<br>- Comparison with other auto-active program verifiers (SPARK, F*, Why3,<br> Viper, Whiley, ...)<br>- Comparison with other proof assistants (Coq, Isabelle/HOL, Lean, ...)<br><br>-----------------------------------------------------------------------------------------------------------<br>** IMPORTANT DATES<br>-----------------------------------------------------------------------------------------------------------<br><br>- Submission: Wednesday, October 18, 2023 (AoE)<br>- Notification: Wednesday, November 15, 2023<br>- Workshop: Sunday, January 14, 2024<br><br>-----------------------------------------------------------------------------------------------------------<br>** ORGANISATION<br>-----------------------------------------------------------------------------------------------------------<br><br>Program Chairs:<br>- Joseph Tassarotti (New York University)<br>- Stefan Zetzsche (Amazon Web Services)<br><br>Program Committee:<br>- Adam Chlipala (Massachusetts Institute of Technology)<br>- Jean-Christophe Filliatre (CNRS)<br>- Andrea Lattuada (VMware Research Group)<br>- Elaine Li (New York University)<br>- Peter Müller (ETH Zurich)<br>- Nadia Polikarpova (University of California, San Diego)<br><br>Steering Committee:<br>- Rustan Leino (Amazon Web Services)<br>- Jean-Baptiste Tristan (Amazon Web Services)<br><br>-----------------------------------------------------------------------------------------------------------<br>** SUBMISSION GUIDELINES<br>-----------------------------------------------------------------------------------------------------------<br><br>To give a presentation at the workshop, please submit an anonymous extended<br>abstract (2-6 pages, excluding references) via hotcrp:<br><br><a href="https://urldefense.com/v3/__https://dafny24.hotcrp.com/__;!!IBzWLUs!S-gSuH3NQU2QznUp_Jeoxu5kNz5g8YNUhbPKmZ-h2qYF-1gigzoFGvRai2cK4UvhCUrAMhkYSn6n2KnNmm1Gq_8bxoIPmz-I_skQc7A$">https://dafny24.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!S-gSuH3NQU2QznUp_Jeoxu5kNz5g8YNUhbPKmZ-h2qYF-1gigzoFGvRai2cK4UvhCUrAMhkYSn6n2KnNmm1Gq_8bxoIPmz-IKmst2YY$">https://www.sigplan.org/Resources/Author/</a><br><br>We don’t intend to publish the workshop’s submissions. However, presentations<br>may be recorded and the videos may be made publicly available.<br><br>-----------------------------------------------------------------------------------------------------------<br>** CONTACT<br>-----------------------------------------------------------------------------------------------------------<br><br>All questions about submission should be emailed to the program chairs Stefan<br>Zetzsche (<a href="mailto:stefanze@amazon.com">stefanze@amazon.com</a>) and Joseph Tassarotti (<a href="mailto:jt4767@nyu.edu">jt4767@nyu.edu</a>).<div><br></div></body></html>