Overview
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:
- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and under-approximation, …
- Interactive theorem proving and SMT automation
- Coinduction and corecursion
- Dynamic frames vs. separation logic vs. ownership
- Test generation for Dafny
- Specification and proof inference for Dafny
- Extensions and applications of Dafny
- Alternative verifier backends
- Program verification at industry-scale
- Translation to or from Dafny and other languages
- Logical foundations for Dafny (partial functions, nonempty types, extreme predicates, …)
- Dafny in teaching
- Comparison with other auto-active program verifiers (SPARK, F*, Why3, Viper, Whiley, …)
- Comparison with other proof assistants (Coq, Isabelle/HOL, Lean, …)
Plenary
Sun 14 JanDisplayed time zone: London change
Sun 14 Jan
Displayed time zone: London change
09:00 - 10:30 | |||
09:00 10mDay opening | Day opening Dafny | ||
09:10 60mKeynote | Verifying a concurrent file system with sequential reasoning Dafny Tej Chajed UW-Madison | ||
10:12 18mTalk | Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking Dafny Alessandro Cimatti Fondazione Bruno Kessler, Alberto Griggio Fondazione Bruno Kessler, Gianluca Redondi Fondazione Bruno Kessler | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:30 | |||
11:00 18mTalk | Dafny Test Generationremote Dafny Aleksandr Fedchin Tufts University, Jeffrey S. Foster Tufts University, Zvonimir Rakamaric Amazon Web Services, Aaron Tomb Amazon Web Services | ||
11:18 18mTalk | Randomised Testing of the Dafny Compiler Dafny Alastair F. Donaldson Imperial College London, Dilan Sheth Imperial College London, Jean-Baptiste Tristan Amazon Web Services, Alex Usher Imperial College London | ||
11:36 18mTalk | Teaching Logic and Set Theory with Dafny Dafny Ran Ettinger NVIDIA and Ben-Gurion University of the Negev and Israel Academic College in Ramat Gan, Hezi Daniel Israel Academic College in Ramat Gan | ||
11:54 18mTalk | Learn 'em Dafny Dafny James Noble Creative Research & Programming Pre-print | ||
12:12 18mTalk | Colouring Flags with Dafny & Idris Dafny | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | Proof Stability / Brittleness / ScaleDafny at Turing Lecture Chair(s): Stefan Zetzsche Amazon Web Services | ||
14:00 18mTalk | Enhancing Proof Stability Dafny Sean McLaughlin Amazon Web Services, Georges-Axel Jaloyan Amazon Web Services, Tongtong Xiang Amazon Web Services, Florian Rabe Amazon Web Services | ||
14:18 18mTalk | Improving the Stability of Type Safety Proofs in Dafny Dafny Joseph W. Cutler University of Pennsylvania, Michael Hicks Amazon Web Services and the University of Maryland, Emina Torlak Amazon Web Services, USA | ||
14:36 18mTalk | Incremental Proof Development in Dafny with Module-Based Induction Dafny | ||
14:54 18mTalk | Portfolio Solving for Dafny Dafny Eric Mugnier University of California San Diego, Sean McLaughlin Amazon Web Services, Aaron Tomb Amazon Web Services | ||
15:12 18mTalk | Domesticating Automation Dafny Pranav Srinivasan University of Michigan / VMware Research, Oded Padon VMware Research, Jon Howell VMware Research, Andrea Lattuada VMware Research | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | Probabilistic Programs and Testing / Verifying ContractsDafny at Turing Lecture Chair(s): Joseph Tassarotti NYU | ||
16:00 18mTalk | VMC: a Dafny Library for Verified Monte Carlo Algorithms Dafny Fabian Zaiser University of Oxford, Stefan Zetzsche Amazon Web Services, Jean-Baptiste Tristan Amazon Web Services | ||
16:18 18mTalk | Caesar: A Verifier for Probabilistic Programs Dafny Philipp Schröer RWTH Aachen University, Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU | ||
16:36 18mTalk | Verifying Dafny Contract Integrity Dafny | ||
16:54 18mTalk | Testing Specifications In Dafny Dafny Eli Goldweber University Of Michigan, Weixin Yu University Of Michigan, Armin Vakil University Of Michigan, Manos Kapritsos University of Michigan, USA | ||
17:30 - 18:15 | |||
17:30 18mTalk | Generation of Verified Assembly Code Using Dafny and Reinforcement Learning Dafny | ||
17:48 18mTalk | CLOVER: Closed-Loop Verifiable Code Generation Dafny Chuyue Sun Stanford University, Ying Sheng Stanford University, Oded Padon VMware Research, Clark Barrett Stanford University | ||
18:06 9mDay closing | Day closing Dafny | ||
Accepted Papers
Call for Papers
We don’t intend to publish the workshop’s submissions. However, presentations may be recorded and the videos may be made publicly available.
Important Dates
- Submission: Wednesday, October 18
11, 2023 (AoE) - Notification: Wednesday, November 15, 2023
- Workshop: Sunday, January 14, 2024
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 chairs Stefan Zetzsche (stefanze@amazon.com) and Joseph Tassarotti (jt4767@nyu.edu).
Social
There are many pubs around the POPL venue. We are planning to meet at “The Coal Hole” (which is 3min away) around 6:45pm.
Address: 91-92 Strand, Greater, London WC2R 0DW
Important Dates AoE (UTC-12h)
| Sun 14 Jan 2024 Workshop |
| Wed 15 Nov 2023 Notification |
| Wed 18 Oct 2023 Submission |
Submission Link
Adam ChlipalaProgramme Committee
Massachusetts Institute of Technology
United States
Jean-Christophe FilliatreProgramme Committee
CNRS
France
Andrea LattuadaProgramme Committee
VMware Research
Switzerland
Elaine LiProgramme Committee
NYU
United States
Peter MüllerProgramme Committee
ETH Zurich
Switzerland
Nadia PolikarpovaProgramme Committee
University of California at San Diego
United States
