<div dir="ltr">-----------------------------------------------------------------------------------------------------------------------------------<br>**<br>**    CALL FOR PARTICIPATION<br>**<br>**    Dafny at POPL 2025<br>**    2nd Workshop on the Dafny Programming and Verification Language<br>**    19th of January 2025, Denver, Colorado, United States<br>**<br>**    <a href="https://urldefense.com/v3/__https://popl25.sigplan.org/home/dafny-2025__;!!IBzWLUs!QJAQkFHQtn326wtRfIxosJIDMgdCQJ9RBG0ya139khBddTHmBNa95Ps7vVjrjE1axycmZTRTHE1ba6m9VCL02zkL0oVFsNqLu3lzkwA$">https://popl25.sigplan.org/home/dafny-2025</a><br>**<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** ACCEPTED PAPERS<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>- Baking for Dafny: A CakeML Backend for Dafny<br>- Dafny as Verification-Aware Intermediate Language for Code Generation<br>- dafny-annotator: AI-Assisted Verification of Dafny Programs<br>- DafnyBench: A Benchmark for Formal Software Verification<br>- Dockyard: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems<br>- Helping users to reduce Brittleness in their Dafny programs - a success story<br>- Laurel: Unblocking Automated Verification with Large Language Models<br>- Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean<br>- Performant, Readable and Interoperable Rust from Dafny<br>- Randomised Testing of the Dafny Compiler: Into the CI<br>- Teaching Types and Non-Interference in Dafny<br>- Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming<br>- Towards Proof Stability in SMT-based Program Verification<br>- Verifying the Fisher-Yates Shuffle Algorithm in Dafny<br>- VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search<br>- Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** ORGANISATION<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>Program Committee Chairs:<br>- Stefan Zetzsche (Amazon Web Services)<br><br>Program Committee:<br>- Seth Ahrenbach (Beneficial AI Foundation)<br>- Tej Chajed (University of Wisconsin–Madison)<br>- Alastair F. Donaldson (Imperial College London)<br>- Marie Farrell (The University of Manchester)<br>- Bryan Parno (Carnegie Mellon University)<br>- Clément Pit-Claudel (EPFL)<br><br>Steering Committee Chairs:<br>- Rustan Leino (Amazon Web Services)<br>- Joseph Tassarotti (New York University)<br>- Jean-Baptiste Tristan (Amazon Web Services)<br><br>-----------------------------------------------------------------------------------------------------------------------------------<br>** CONTACT<br>-----------------------------------------------------------------------------------------------------------------------------------<br><br>All questions should be emailed to the program chair Stefan Zetzsche (<a href="mailto:stefanze@amazon.com">stefanze@amazon.com</a>).</div>