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

[Stefan Zetzsche]

-----------------------------------------------------------------------------------------------------------------------------------
**    *Update: Submission deadline extended*
-----------------------------------------------------------------------------------------------------------------------------------
**
**    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 22, 2025
**
**    https://urldefense.com/v3/__https://popl26.sigplan.org/home/dafny-2026__;!!IBzWLUs!XbigvqHwhJn9rH_fZ5vdD08W3SR2wRzAOdxMNlDDq_leZgnYhw1zoVpE_H_CcAAZH18VfrmICNRQpRFlNZanbbXm1HgTrhiyBp4Wt2M$ 
**    https://urldefense.com/v3/__https://dafny26.hotcrp.com__;!!IBzWLUs!XbigvqHwhJn9rH_fZ5vdD08W3SR2wRzAOdxMNlDDq_leZgnYhw1zoVpE_H_CcAAZH18VfrmICNRQpRFlNZanbbXm1HgTrhiyC7a741I$ 
**
-----------------------------------------------------------------------------------------------------------------------------------

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.
Auto-active tools also
exist for other languages like C, Java or Rust. 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 22, 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!XbigvqHwhJn9rH_fZ5vdD08W3SR2wRzAOdxMNlDDq_leZgnYhw1zoVpE_H_CcAAZH18VfrmICNRQpRFlNZanbbXm1HgTrhiyC7a741I$ 

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!XbigvqHwhJn9rH_fZ5vdD08W3SR2wRzAOdxMNlDDq_leZgnYhw1zoVpE_H_CcAAZH18VfrmICNRQpRFlNZanbbXm1HgTrhiy3Ylnb2g$ 

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.

-----------------------------------------------------------------------------------------------------------------------------------
** KEYNOTE
-----------------------------------------------------------------------------------------------------------------------------------

Speaker: Karthikeyan Bhargavan (Inria/Cryspen)

Title: Software Verification meets Real-World Cryptography

Abstract: In recent years, several software verification frameworks have
been applied to analyze
the correctness and security of implementations of cryptographic algorithms
and protocols, with
some notable successes. I will describe what makes the analysis of
real-world cryptography
interesting and challenging for formal verification, using examples from
several research and
commercial projects I have participated in. We will discuss the limits of
what can be proved today,
what remains to be done, and what challenges I see on the horizon.

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

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

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/20251002/9261fa95/attachment.htm>