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

[Stefan Zetzsche]

-----------------------------------------------------------------------------------------------------------------------------------
**
**    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://urldefense.com/v3/__https://popl25.sigplan.org/home/dafny-2025__;!!IBzWLUs!QJAQkFHQtn326wtRfIxosJIDMgdCQJ9RBG0ya139khBddTHmBNa95Ps7vVjrjE1axycmZTRTHE1ba6m9VCL02zkL0oVFsNqLu3lzkwA$ 
**
-----------------------------------------------------------------------------------------------------------------------------------

-----------------------------------------------------------------------------------------------------------------------------------
** 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 at amazon.com).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20250117/cb8ccd34/attachment.htm>