About
Dafny is a verification-aware programming language that has native support for specifications and proofs, and is equipped with an auto-active static program verifier. The workshop aims to provide a platform for reports about applications of Dafny in industry, research on programming-language concepts that are relevant to Dafny, and talks about Dafny’s role in teaching. Topics include but are not limited to the following:
- Alternative verifier backends
- Coinduction and corecursion
- Comparison with other auto-active program verifiers (SPARK, F*, Why3, Viper, Whiley, …)
- Comparison with other proof assistants (Coq, Isabelle/HOL, Lean, …)
- Dafny in teaching
- Dynamic frames vs. separation logic vs. ownership
- Extensions and applications of Dafny
- Interactive theorem proving and SMT automation
- Logical foundations for Dafny (partial functions, nonempty types, extreme predicates, …)
- Program verification at industry-scale
- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and under-approximation, …
- Specification and proof inference for Dafny
- Test generation for Dafny
- Translation to or from Dafny and other languages
This program is tentative and subject to change.
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 Nada Amin Harvard University | ||
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 | ||
11:54 18mTalk | Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant Systems Dafny Derek Leung MIT, 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 | ||
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 | ||
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 | ||
Accepted Papers
Call for Papers
The workshop won’t have formal proceedings. However, presentations may be recorded and the videos may be made publicly available. You are free to submit work for presentation that is or will be published elsewhere.
Important Dates
Submission: Wednesday, October 16 30, 2024 (AoE)
Notification: Wednesday, November 20, 2024
Workshop: Sunday, January 19, 2025
Submission Guidelines
To give a presentation at the workshop, please submit an anonymous extended abstract (2-6 pages, excluding references) via hotcrp:
Please use the acmart two-column sigplan sub-format LaTeX style to prepare your submission:
https://www.sigplan.org/Resources/Author/
Contact
All questions about submission should be emailed to the program chair Stefan Zetzsche (stefanze@amazon.com).
Important Dates AoE (UTC-12h)
| Sun 19 Jan 2025 Workshop |
| Wed 20 Nov 2024 Notification |
| Wed 30 Oct 2024 Submission |
Submission Link
Seth AhrenbachPC Member
Beneficial AI Foundation
United States
Tej ChajedPC Member
UW-Madison
United States
Alastair F. DonaldsonPC Member
Imperial College London
United Kingdom
Marie FarrellPC Member
The University of Manchester
United Kingdom
Bryan ParnoPC Member
Carnegie Mellon University
United States
Clément Pit-ClaudelPC Member
EPFL
Switzerland
