The Coq mailing list

[Stefan Zetzsche <stefanzetzsche AT gmail.com>]

-----------------------------------------------------------------------------------------------------------------------------------
**
**    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://popl26.sigplan.org/home/dafny-2026
**    https://dafny26.hotcrp.com
**
-----------------------------------------------------------------------------------------------------------------------------------

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 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://dafny26.hotcrp.com

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

https://www.sigplan.org/Resources/Author/

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).