Dafny 2024
as the organisers put it
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 core ...
who it's for
Dafny users and contributors, verification engineers, programming language researchers, software engineers applying formal verification, university instructors in formal methods, Dafny compiler developers, SMT and theorem prover engineers
topics
concurrent file system verification; parameterized interlocking logic; counterexample-based test generation; differential and metamorphic compiler fuzzing; teaching logic with Dafny; proof stability and robustness techniques; module-based induction patterns; portfolio SMT solving in the cloud; probabilistic program verification libraries; verified assembly generation with reinforcement learning; closed-loop verifiable code generation
| title | author | length |
|---|---|---|
| Day opening | Stefan Zetzsche, Joseph Tassarotti | 04m |
This session delivers logistics and a roadmap not technical results: 18 talks across five sessions, running 9:00–6:00 with 15+3 minute slots, plus Q&A and… | ||
| Verifying a concurrent file system with sequential reasoning | Tej Chajed | 01h 07m |
A verified concurrent NFS server called DaisyNFS implements linearizability and crash durability by building file-system logic as atomic transactions atop a… | ||
| Towards the verification of a generic interlocking logic: Dafny meets parameter... | Alessandro Cimatti, Alberto Griggio, Gianluca Redondi | 20m |
A generic interlocking logic is encoded in Dafny alongside the tool’s C/Python output, and a parameterized model checker is used to synthesize inductive… | ||
| Dafny Test Generation | Aleksandr Fedchin, Jeffrey S. Foster, Zvonimir Rakamaric, Aaron Tomb | 17m |
DTest generates executable unit and system tests by inserting failing assertions, asking the Dafny verifier for counterexamples, and extracting concrete inputs… | ||
| Randomised Testing of the Dafny Compiler | Alastair F. Donaldson, Dilan Sheth, Jean-Baptiste Tristan, Alex Usher | 16m |
Built two generators, fuzz-d (differential testing) and DafnyFuzz (metamorphic testing), plus comparison with XDsmith, and apply reconditioning and… | ||
| Teaching Logic and Set Theory with Dafny | Ran Ettinger, Hezi Daniel | 21m |
Course materials use Dafny as a teaching assistant and programming language plus proof assistant to give instant feedback on assignments and to speed grading… | ||
| Learn 'em Dafny | James Noble | 19m |
A programming‑first software correctness course uses Dafny with a flipped classroom and automated, proof‑based feedback for about 120 required students… | ||
| Colouring Flags with Dafny & Idris | Jan de Muijnck-Hughes, James Noble | 19m |
Compares Dafny’s imperative design-by-contract + Hoare/Boogie pipeline with Idris’s dependently typed, type-driven approach by reimplementing the Dutch… | ||
| Enhancing Proof Stability | Sean McLaughlin, Georges-Axel Jaloyan, Tongtong Xiang, Florian Rabe | 21m |
Claim: simple, low-automation proofs break less often. Implements a coding style called Dafny64 that makes invariants opaque, moves postconditions into… | ||
| Improving the Stability of Type Safety Proofs in Dafny | Joseph W. Cutler, Michael Hicks, Emina Torlak | 20m |
Presents a concrete method for stabilizing Dafny type-soundness proofs by making the safety predicate and then the typechecker opaque, proving small safety… | ||
| Incremental Proof Development in Dafny with Module-Based Induction | Son Ho, Clément Pit-Claudel | 16m |
Claim: encoding Coq-style induction principles as module-based induction in Dafny makes iterative proofs stable and debuggable. Implementation: a list… | ||
| Portfolio Solving for Dafny | Eric Mugnier, Sean McLaughlin, Aaron Tomb | 18m |
A cloud-hosted portfolio runs multiple SMT engines (Z3 4.2.1, 4.8.5, newer Z3, CVC5, Vampire) against the same 177k‑LOC Dafny repo with ~14k VCs and returns… | ||
| Domesticating Automation | Pranav Srinivasan, Oded Padon, Jon Howell, Andrea Lattuada | 15m |
Proposes a module-granular view of the quantifier instantiation graph and a crude metric that ranks modules by how many downstream instantiations they enable… | ||
| VMC: a Dafny Library for Verified Monte Carlo Algorithms | Fabian Zaiser, Stefan Zetzsche, Jean-Baptiste Tristan | 18m |
Open-source Dafny library that provides verified Monte Carlo samplers: each sampler has a bitstream-to-value functional model, a machine-checked proof that the… | ||
| Caesar: A Verifier for Probabilistic Programs | Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja | 18m |
A deductive verifier called Caesar implements a probabilistic Boogie‑style pipeline: programs, specifications and proof rules are encoded in the quantitative… | ||
| Verifying Dafny Contract Integrity | Cassidy Waldrip, Eric Mercer | 19m |
Tool automatically inserts Dafny-generated assertions (via Dafny rewriters) and asks Boogie/Z3 whether four specific pitfalls occur: contradiction, vacuity… | ||
| Testing Specifications In Dafny | Eli Goldweber, Weixin Yu, Armin Vakil, Manos Kapritsos | 17m |
IronSpec provides concrete ways to surface specification bugs in Dafny: an automatic sanity checker that flags input/output disconnects, an automated mutation… | ||
| Generation of Verified Assembly Code Using Dafny and Reinforcement Learning | Christopher Brix, Jean-Baptiste Tristan | 18m |
Reinforcement learning generates assembly programs while a Dafny model of machine state automatically verifies input-output properties, turning testing into… | ||
| CLOVER: Closed-Loop Verifiable Code Generation | Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett | 20m |
Generates code, docstrings, and formal annotations with GPT‑4 then applies six directed consistency checks (using reconstruction testing and the Dafny… | ||
| Day closing | Stefan Zetzsche, Joseph Tassarotti | 01m |
Day closing gives practical logistics and requests: organizers ask for written feedback for future conferences and topics, note a planned meetup at 6:45 at the… | ||
| nothing matches | ||