Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] (Call for Participation) Dafny Workshop at POP...

Email Gateway (Jan 17 2025 at 17:28):

From: Stefan Zetzsche <stefanzetzsche@gmail.com>

**
** CALL FOR PARTICIPATION
**
** Dafny at POPL 2025
** 2nd Workshop on the Dafny Programming and Verification Language
** 19th of January 2025, Denver, Colorado, United States
**
** https://popl25.sigplan.org/home/dafny-2025
**

** ACCEPTED PAPERS

• Baking for Dafny: A CakeML Backend for Dafny
• Dafny as Verification-Aware Intermediate Language for Code Generation
• dafny-annotator: AI-Assisted Verification of Dafny Programs
• DafnyBench: A Benchmark for Formal Software Verification

• Dockyard: A Modular Framework for Verifying Liveness of Byzantine Fault
  Tolerant Systems

• Helping users to reduce Brittleness in their Dafny programs - a success
  story

• Laurel: Unblocking Automated Verification with Large Language Models

• Lean on Dafny: Exploring Interactive Verification of Dafny Programs in
  Lean

• Performant, Readable and Interoperable Rust from Dafny

• Randomised Testing of the Dafny Compiler: Into the CI
• Teaching Types and Non-Interference in Dafny
• Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
• Towards Proof Stability in SMT-based Program Verification
• Verifying the Fisher-Yates Shuffle Algorithm in Dafny

• VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large
  Language Model, and Tree Search

• Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny

** ORGANISATION

Program Committee Chairs:

• Stefan Zetzsche (Amazon Web Services)

Program Committee:

• Seth Ahrenbach (Beneficial AI Foundation)
• Tej Chajed (University of Wisconsin–Madison)
• Alastair F. Donaldson (Imperial College London)
• Marie Farrell (The University of Manchester)
• Bryan Parno (Carnegie Mellon University)
• Clément Pit-Claudel (EPFL)

Steering Committee Chairs:

• Rustan Leino (Amazon Web Services)
• Joseph Tassarotti (New York University)
• Jean-Baptiste Tristan (Amazon Web Services)

** CONTACT

All questions should be emailed to the program chair Stefan Zetzsche (
stefanze@amazon.com).

Email Gateway (Jan 06 2026 at 12:31):

From: Stefan Zetzsche <stefanzetzsche@gmail.com>

**
** CALL FOR PARTICIPATION
**
** Dafny at POPL 2026
** 3rd Workshop on Auto-active Programming and Verification Languages
** January 11, 2026. Rennes, France
**
** https://popl26.sigplan.org/home/dafny-2026
**

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@gmail.com) or Stefan Zetzsche (stefanzetzsche@gmail.com).

Last updated: Jan 11 2026 at 16:28 UTC