<div dir="ltr">-----------------------------------------------------------------------------------------------------------------------------------<br>**<br>**    CALL FOR EXTENDED ABSTRACTS<br>**<br>**    Dafny at POPL 2026<br>**    3rd Workshop on Auto-active Programming and Verification Languages<br>**    January 11, 2026. Rennes, France<br>**<br>**    Submission Deadline:<br>**    October 8, 2025<br>**<br>**    <a href="https://urldefense.com/v3/__https://popl26.sigplan.org/home/dafny-2026__;!!IBzWLUs!WZSiFMj-oOyNre5V_EU_KnOJN0nlLi9EbPU_L2x-yCimFDa8kQLyRUZyP4lYHIcRmEmVZeNiwpEy0MJ9lblKQk00PndMXDq6_F8wFlg$">https://popl26.sigplan.org/home/dafny-2026</a><br>**    <a href="https://urldefense.com/v3/__https://dafny26.hotcrp.com__;!!IBzWLUs!WZSiFMj-oOyNre5V_EU_KnOJN0nlLi9EbPU_L2x-yCimFDa8kQLyRUZyP4lYHIcRmEmVZeNiwpEy0MJ9lblKQk00PndMXDq6ruudDwE$">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 Dafny, SPARK, F*, Why3, Viper, Whiley. The workshop aims to </div><div>be a forum for all auto-active 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 8, 2025<br>- Notification: Wednesday, November 12, 2025<br>- Workshop: Sunday, January 11, 2026<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://dafny26.hotcrp.com__;!!IBzWLUs!WZSiFMj-oOyNre5V_EU_KnOJN0nlLi9EbPU_L2x-yCimFDa8kQLyRUZyP4lYHIcRmEmVZeNiwpEy0MJ9lblKQk00PndMXDq6ruudDwE$">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!WZSiFMj-oOyNre5V_EU_KnOJN0nlLi9EbPU_L2x-yCimFDa8kQLyRUZyP4lYHIcRmEmVZeNiwpEy0MJ9lblKQk00PndMXDq6r-rFjI0$">https://www.sigplan.org/Resources/Author/</a><br><br>The workshop won’t have formal proceedings. However, presentations may be recorded and the <br>videos may be made publicly available. You are free to submit work for presentation that is or will <br>be published elsewhere.<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** ORGANISATION<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>Program Committee:<br>- Yann Herklotz (EPFL)<br>- Jacques-Henri Jourdan (CNRS)<br>- Georges-Axel Jaloyan (Corps des Mines)<br>- Ilya Sergey (National University of Singapore)<br>- Thierry Lecomte (ClearSy)<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">yannick.moy@gmail.com</a>) or Stefan Zetzsche (<a href="mailto:stefanzetzsche@gmail.com">stefanzetzsche@gmail.com</a>).</div><div><br></div></div>