[TYPES/announce] (CfP) Dafny Workshop at POPL 2026

[Stefan Zetzsche]

-----------------------------------------------------------------------------------------------------------------------------------
**
**    CALL FOR EXTENDED ABSTRACTS
**
**    Dafny at POPL 2026
**    3rd Workshop on Auto-active Programming and Verification Languages
**    January 11, 2026. Rennes, France
**
**    Submission Deadline:
**    October 8, 2025
**
**    https://urldefense.com/v3/__https://popl26.sigplan.org/home/dafny-2026__;!!IBzWLUs!WZSiFMj-oOyNre5V_EU_KnOJN0nlLi9EbPU_L2x-yCimFDa8kQLyRUZyP4lYHIcRmEmVZeNiwpEy0MJ9lblKQk00PndMXDq6_F8wFlg$ 
**    https://urldefense.com/v3/__https://dafny26.hotcrp.com__;!!IBzWLUs!WZSiFMj-oOyNre5V_EU_KnOJN0nlLi9EbPU_L2x-yCimFDa8kQLyRUZyP4lYHIcRmEmVZeNiwpEy0MJ9lblKQk00PndMXDq6ruudDwE$ 
**
-----------------------------------------------------------------------------------------------------------------------------------

There is an established group of verification-aware programming languages
that have native
support for specifications and proofs, and are equipped with an auto-active
static program verifier.
Examples of such languages are Dafny, SPARK, F*, Why3, Viper, Whiley. The
workshop aims to
be a forum for all auto-active program verifiers and their related
techniques.

Topics include but are not limited to the following:
- AI for verification and vice versa
- Alternative verifier backends
- Coinduction and corecursion
- Comparison with interactive proof assistants (Rocq, Isabelle/HOL, Lean, …)
- Dynamic frames vs. separation logic vs. ownership
- Extensions and applications of the auto-active language
- GUI and IDE for auto-active verification
- User interaction features
- Logical foundations (partial functions, nonempty types, extreme
predicates, …)
- Program verification at industry-scale
- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and
under-approximation, …
- SMT automation
- Specification and proof inference for the auto-active language
- Test generation
- Translation to or from the auto-active language
- Verification in teaching

-----------------------------------------------------------------------------------------------------------------------------------
** IMPORTANT DATES
-----------------------------------------------------------------------------------------------------------------------------------

- Submission: Wednesday, October 8, 2025
- Notification: Wednesday, November 12, 2025
- Workshop: Sunday, January 11, 2026

-----------------------------------------------------------------------------------------------------------------------------------
** SUBMISSION GUIDELINES
-----------------------------------------------------------------------------------------------------------------------------------

To give a presentation at the workshop, please submit an anonymous extended
abstract
(2-6 pages, excluding references) via hotcrp:

https://urldefense.com/v3/__https://dafny26.hotcrp.com__;!!IBzWLUs!WZSiFMj-oOyNre5V_EU_KnOJN0nlLi9EbPU_L2x-yCimFDa8kQLyRUZyP4lYHIcRmEmVZeNiwpEy0MJ9lblKQk00PndMXDq6ruudDwE$ 

Please use the acmart two-column sigplan sub-format LaTeX style to prepare
your submission:

https://urldefense.com/v3/__https://www.sigplan.org/Resources/Author/__;!!IBzWLUs!WZSiFMj-oOyNre5V_EU_KnOJN0nlLi9EbPU_L2x-yCimFDa8kQLyRUZyP4lYHIcRmEmVZeNiwpEy0MJ9lblKQk00PndMXDq6r-rFjI0$ 

The workshop won’t have formal proceedings. However, presentations may be
recorded and the
videos may be made publicly available. You are free to submit work for
presentation that is or will
be published elsewhere.

-----------------------------------------------------------------------------------------------------------------------------------
** ORGANISATION
-----------------------------------------------------------------------------------------------------------------------------------

Program Committee:
- Yann Herklotz (EPFL)
- Jacques-Henri Jourdan (CNRS)
- Georges-Axel Jaloyan (Corps des Mines)
- Ilya Sergey (National University of Singapore)
- Thierry Lecomte (ClearSy)

Program Committee Chairs:
- Yannick Moy (ANSSI)
- Stefan Zetzsche (Amazon Web Services)

Steering Committee Chairs:
- Olivier Bouissou (Amazon Web Services)
- Rustan Leino (Amazon Web Services)
- Joseph Tassarotti (New York University)
- Jean-Baptiste Tristan (Amazon Web Services)

-----------------------------------------------------------------------------------------------------------------------------------
** CONTACT
-----------------------------------------------------------------------------------------------------------------------------------

All questions about submission should be emailed to the program chairs
Yannick Moy
(yannick.moy at gmail.com) or Stefan Zetzsche (stefanzetzsche at gmail.com).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20250820/924046c2/attachment-0001.htm>