<div dir="ltr">-----------------------------------------------------------------------------------------------------------------------------------<br>**    <b>Update: Submission deadline extended</b><br>-----------------------------------------------------------------------------------------------------------------------------------<br>**<br>**    CALL FOR EXTENDED ABSTRACTS<br>**<br>**    <span class="gmail-il">Dafny</span> at POPL 2026<br>**    3rd <span class="gmail-il">Workshop</span> on Auto-active Programming and Verification Languages<br>**    January 11, 2026. Rennes, France<br>**<br>**    Submission Deadline:<br>**    October 22, 2025<br>**<br>**    <a href="https://urldefense.com/v3/__https://popl26.sigplan.org/home/dafny-2026__;!!IBzWLUs!XbigvqHwhJn9rH_fZ5vdD08W3SR2wRzAOdxMNlDDq_leZgnYhw1zoVpE_H_CcAAZH18VfrmICNRQpRFlNZanbbXm1HgTrhiyBp4Wt2M$" target="_blank">https://popl26.sigplan.org/home/<span class="gmail-il">dafny</span>-2026</a><br>**    <a href="https://urldefense.com/v3/__https://dafny26.hotcrp.com/__;!!IBzWLUs!XbigvqHwhJn9rH_fZ5vdD08W3SR2wRzAOdxMNlDDq_leZgnYhw1zoVpE_H_CcAAZH18VfrmICNRQpRFlNZanbbXm1HgTrhiyYi9m_KQ$" target="_blank">https://dafny26.hotcrp.com</a><br>**<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>There is an established group of verification-aware programming languages that have native <div>support for specifications and proofs, and are equipped with an auto-active static program verifier. </div><div>Examples of such languages are <span class="gmail-il">Dafny</span>, SPARK, F*, Why3, Viper, Whiley. Auto-active tools also </div><div>exist for other languages like C, Java or Rust. The <span class="gmail-il">workshop</span> aims to be a forum for all auto-active </div><div>program verifiers and their related techniques.<br><br>Topics include but are not limited to the following:<br>- AI for verification and vice versa<br>- Alternative verifier backends<br>- Coinduction and corecursion<br>- Comparison with interactive proof assistants (Rocq, Isabelle/HOL, Lean, …)<br>- Dynamic frames vs. separation logic vs. ownership<br>- Extensions and applications of the auto-active language<br>- GUI and IDE for auto-active verification<br>- User interaction features<br>- Logical foundations (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>- SMT automation<br>- Specification and proof inference for the auto-active language<br>- Test generation<br>- Translation to or from the auto-active language<br>- Verification in teaching<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** IMPORTANT DATES<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>- Submission: Wednesday, October 22, 2025<br>- Notification: Wednesday, November 12, 2025<br>- <span class="gmail-il">Workshop</span>: Sunday, January 11, 2026<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** SUBMISSION GUIDELINES<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>To give a presentation at the <span class="gmail-il">workshop</span>, please submit an anonymous extended abstract<br>(2-6 pages, excluding references) via hotcrp:<br><br><a href="https://urldefense.com/v3/__https://dafny26.hotcrp.com/__;!!IBzWLUs!XbigvqHwhJn9rH_fZ5vdD08W3SR2wRzAOdxMNlDDq_leZgnYhw1zoVpE_H_CcAAZH18VfrmICNRQpRFlNZanbbXm1HgTrhiyYi9m_KQ$" target="_blank">https://dafny26.hotcrp.com</a><br><br>Please use the acmart two-column sigplan sub-format LaTeX style to prepare your submission:<br><br><a href="https://urldefense.com/v3/__https://www.sigplan.org/Resources/Author/__;!!IBzWLUs!XbigvqHwhJn9rH_fZ5vdD08W3SR2wRzAOdxMNlDDq_leZgnYhw1zoVpE_H_CcAAZH18VfrmICNRQpRFlNZanbbXm1HgTrhiy3Ylnb2g$" target="_blank">https://www.sigplan.org/Resources/Author/</a><br><br>The <span class="gmail-il">workshop</span> won’t have formal proceedings. However, presentations may be recorded and the<br>videos may be made publicly available. You are free to submit <span class="gmail-il">work</span> for presentation that is or will<br>be published elsewhere.<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** KEYNOTE<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>Speaker: Karthikeyan Bhargavan (Inria/Cryspen)</div><div><br>Title: Software Verification meets Real-World Cryptography</div><div><br>Abstract: In recent years, several software verification frameworks have been applied to analyze </div><div>the correctness and security of implementations of cryptographic algorithms and protocols, with </div><div>some notable successes. I will describe what makes the analysis of real-world cryptography </div><div>interesting and challenging for formal verification, using examples from several research and </div><div>commercial projects I have participated in. We will discuss the limits of what can be proved today, </div><div>what remains to be done, and what challenges I see on the horizon.</div><div><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** ORGANISATION<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>Program Committee:<br>- Yann Herklotz (EPFL)<br>- Georges-Axel Jaloyan (Corps des Mines)<br>- Jacques-Henri Jourdan (CNRS)<br>- Thierry Lecomte (ClearSy)<br>- Ilya Sergey (National University of Singapore)<br>- Fabian Zaiser (MIT)<br><br>Program Committee Chairs:<br>- Yannick Moy (ANSSI)<br>- Stefan Zetzsche (Amazon Web Services)<br><br>Steering Committee Chairs:<br>- Olivier Bouissou (Amazon Web Services)<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 chairs Yannick Moy<br>(<a href="mailto:yannick.moy@gmail.com" target="_blank">yannick.moy@gmail.com</a>) or Stefan Zetzsche (<a href="mailto:stefanzetzsche@gmail.com" target="_blank">stefanzetzsche@gmail.com</a>).</div></div>