POPL 2025 (series) / Dafny 2025 (series) /
Dafny 2025 Program
This is the Dafny 2025 program - see the full program for POPL 2025 and all affiliated events.
Filter Program
Dates
Sun 19 Jan 2025
Rooms
Hopscotch
Tracks
Dafny
Badges
Nothing to filter
Your Program
Nothing to filter
Sun 19 JanDisplayed time zone: Mountain Time (US & Canada) change
Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 10mDay opening | Day opening Dafny Stefan Zetzsche Amazon Web Services | ||
09:10 60mKeynote | Keynote Dafny K. Rustan M. Leino Amazon | ||
11:00 - 12:30 | |||
11:00 18mTalk | Helping users to reduce Brittleness in their Dafny programs - a success story Dafny | ||
11:18 18mTalk | Towards Proof Stability in SMT-based Program Verification Dafny | ||
11:36 18mTalk | Verifying the Fisher-Yates Shuffle Algorithm in Dafny Dafny Stefan Zetzsche Amazon Web Services, Tancrède Lepoint Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services, Mikael Mayer Automated Reasoning Group, Amazon Web Services Pre-print | ||
11:54 18mTalk | Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems Dafny Derek Leung Massachusetts Institute of Technology, USA, Nickolai Zeldovich Massachusetts Institute of Technology, USA, M. Frans Kaashoek Massachusetts Institute of Technology, USA | ||
12:12 18mTalk | Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny Dafny | ||
14:00 - 15:30 | |||
14:00 18mTalk | Baking for Dafny: A CakeML Backend for Dafny Dafny Daniel Nezamabadi Chalmers University of Technology and University of Gothenburg, Magnus O. Myreen Chalmers University of Technology Pre-print | ||
14:18 18mTalk | Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean Dafny Wojciech Różowski University College London, Georges-Axel Jaloyan Amazon Web Services, Sean McLaughlin Amazon Web Services | ||
14:36 18mTalk | Performant, Readable and Interoperable Rust from Dafny Dafny Mikael Mayer Automated Reasoning Group, Amazon Web Services, Shadaj Laddad University of California at Berkeley, Fabio Madge Automated Reasoning Group, Amazon Web Services, Siva Somayyajula Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services | ||
14:54 18mTalk | Randomised Testing of the Dafny Compiler: Into the CI Dafny Karnbongkot Boonriong Imperial College London, Alastair F. Donaldson Imperial College London, Stefan Zetzsche Amazon Web Services | ||
15:12 18mTalk | Teaching Types and Non-Interference in Dafny Dafny Bryan Parno Carnegie Mellon University | ||
16:00 - 18:00 | |||
16:00 18mTalk | Laurel: Unblocking Automated Verification with Large Language Models Dafny Eric Mugnier University of California San Diego, Emmanuel Anaya Gonzalez UCSD, Nadia Polikarpova University of California at San Diego, Ranjit Jhala University of California at San Diego, Zhou Yuanyuan UCSD | ||
16:18 18mTalk | VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search Dafny David Brandfonbrener Harvard, Simon Henniger Technical University of Munich, Sibi Raja Harvard, Tarun Prasad Harvard, Chloe Loughridge Harvard University, Federico Cassano Northeastern University, Sabrina Ruixin Hu Harvard, Jianang Yang Million.js, William E. Byrd University of Alabama at Birmingham, USA, Robert Zinkov University of Oxford, Nada Amin Harvard University | ||
16:36 18mTalk | dafny-annotator: AI-Assisted Verification of Dafny Programs Dafny Gabriel Poesia Stanford University, Chloe Loughridge Harvard University, Nada Amin Harvard University | ||
16:54 18mTalk | Dafny as Verification-Aware Intermediate Language for Code Generation Dafny Yue Chen Li Massachusetts Institute of Technology, Stefan Zetzsche Amazon Web Services, Siva Somayyajula Amazon Web Services Pre-print | ||
17:12 18mTalk | DafnyBench: A Benchmark for Formal Software Verification Dafny Chloe Loughridge Harvard University, Qinyi Sun Massachusetts Institute of Technology, Seth Ahrenbach Beneficial AI Foundation, Federico Cassano Northeastern University, Chuyue Sun Stanford University, Ying Sheng Stanford University, Anish Mudide Massachusetts Institute of Technology, Md Rakib Hossain Misu University of California Irvine, Nada Amin Harvard University, Max Tegmark Massachusetts Institute of Technology | ||
17:30 18mTalk | Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming Dafny Saikat Chakraborty Microsoft Research, Gabriel Ebner Microsoft Research, Siddharth Bhat University of Cambridge, Sarah Fakhoury Microsoft Research, Sakina Fatima University of Ottawa, Shuvendu K. Lahiri Microsoft Research, Nikhil Swamy Microsoft Research | ||
17:48 12mDay closing | Day closing Dafny Stefan Zetzsche Amazon Web Services | ||