[TYPES/announce] (Call for Participation) Dafny Workshop at POPL 2026

[Stefan Zetzsche]

-----------------------------------------------------------------------------------------------------------------------------------
**
**    CALL FOR PARTICIPATION
**
**    Dafny at POPL 2026
**    3rd Workshop on Auto-active Programming and Verification Languages
**    January 11, 2026. Rennes, France
**
**    https://urldefense.com/v3/__https://popl26.sigplan.org/home/dafny-2026__;!!IBzWLUs!QgdPvi_dn88ioU_nxMJ7tLyq2ADGiGSUZZa2mLi4nLh6lGM590QSup-SWak-YTAp-QRxLILkoNfvwfM-ezHNhkjDiX1QaSvxqgC2w3Y$ 
**
-----------------------------------------------------------------------------------------------------------------------------------

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.

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

-----------------------------------------------------------------------------------------------------------------------------------
** ACCEPTED TALKS
-----------------------------------------------------------------------------------------------------------------------------------

- A benchmark for vericoding: formally verified program synthesis
- A Correct-by-Construction Checker for Validation of Railway Data
- ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
- DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
- Diagnostics in Probabilistic Program Verification
- Explicit Abstraction Barrier for Autoactive Verification
- Formal Verification of Minimax Algorithms
- Lessons from Building an Auto-Active Verifier in Lean
- Managing the Proof Context in SPARK
- MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active
Verification
- Specification-Guided Repair of Arithmetic Errors in Dafny Programs using
LLMs
- Teaching Automata Theory and Formal Languages with Dafny
- The Design of an Interactive Proof Mode for Dafny
- Toward Automated, Contamination-free Dafny Benchmark Generation
- Tunable Automation in Automated Program Verification
- Velvet: A Multi-Modal Verifier for Effectful Programs
- Verification of E-Voting Algorithms in Dafny

-----------------------------------------------------------------------------------------------------------------------------------
** 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/20260106/0b75e64a/attachment-0001.htm>