Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs.
The Dafny programming language is designed to support the static verification of programs. It is imperative, sequential, supports generic classes, dynamic allocation, and inductive datatypes, and builds in specification constructs. The specifications include pre- and postconditions, frame specifications (read and write sets), and termination metrics. To further support specifications, the language also offers updatable ghost variables, recursive functions, and types like sets and sequences. Specifications and ghost constructs are used only during verification; the compiler omits them from the executable code.
The Dafny verifier is run as part of the compiler. As such, a programmer interacts with it much in the same way as with the static type checker—when the tool produces errors, the programmer responds by changing the program’s type declarations, specifications, and statements.
The easiest way to try out Dafny is in your web browser at rise4fun. Once you get a bit more serious, you may prefer to download to run it on your machine. Although Dafny can be run from the command line (on Windows or other platforms), the preferred way to run it is in Microsoft Visual Studio 2010, where the Dafny verifier runs in the background while the programmer is editing the program.
From verified programs, the Dafny compiler produces code (.dll or .exe) for the .NET platform. However, the facilities for interfacing with other .NET code are minimal.
The source code for Dafny is available.
To become a user of Dafny, follow the Dafny tutorial online. Or, if you prefer it in a printed format:
Jason Koenig and K. Rustan M. Leino. Getting started with Dafny: a guide. In Marktoberdorf 2011 lecture notes. To appear, 2012. [PDF]
To learn more about the features of Dafny, the Dafny Quick Reference may be for you.
The following paper presents the salient features of Dafny, along with the Schorr-Waite algorithm written in Dafny. If you're scientifically or technically inclined, this is the one to read and cite:
To dig deeper into the technology behind Dafny, the following lecture notes from the Marktoberdorf 2008 summer school describe the encoding of Dafny into Boogie 2:
K. Rustan M. Leino. Specification and verification of object-oriented software. In Engineering Methods and Tools for Software Safety and Security, volume 22 of NATO Science for Peace and Security Series D: Information and Communication Security, pages 231-266. IOS Press, 2009. [PDF] [slides from the lectures]
Benchmarks and competitions
Dafny was a popular tool among the teams at the VSTTE 2012 program verification competition. It was also used at the COST Verification Competition 2011, as part of the FoVeOOS conference. And it was used in the VSComp 2010 competition at VSTTE 2010, from which a report was published:
Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin Weiss. The 1st Verified Software Competition: Experience Report. In FM 2011: Formal Methods - 17th International Symposium on Formal Methods, volume 6664 of LNCS, pages 154-168. Springer, 2011. [PDF]
(which won Best Paper Award at FM 2011). You can find Dafny solutions to the problem sets of these competitions under the Test directory of the Dafny sources.
Dafny has also been used to solve various verification benchmark challenges. At the Verified Software: Tools, Techniques, and Experiments (VSTTE 2008) conference, Weide et al. presented some verification benchmarks to facilitate the comparison between different specification languages and verifiers. This paper describes Dafny programs for those benchmarks:
K. Rustan M. Leino and Rosemary Monahan. Dafny meets the Verification Benchmarks Challenge. In VSTTE 2010, volume 6217 of LNCS, pages 112-126. Springer, 2010. [PDF]
Dafny has also been used to solve some of the VACID-0 verification benchmarks:
K. Rustan M. Leino and Michał Moskal. VACID-0: Verification of Ample Correctness of Invariants of Data-structures, Edition 0. Tools and Experiments workshop at VSTTE 2010. [PDF]
Dafny is being used in teaching. Here's a partial list of universities that are or have been using Dafny in some capacity in lectures and class work:
Caltech, Rajeev Joshi (CS 116)
Lomonosov Moscow State University, Eugene Kornykhin
Kansas State University, Torben Amtoft
Imperial College London, Sophia Drossopoulou and Will Sonnex
NUI Maynooth, Rosemary Monahan
ETH Zurich, Peter Müller
University of Washington, Ethan Jackson; Emina Torlak
University of Iowa, Cesare Tinelli
Koç University, Serdar Taşıran
Rice University, Swarat Chaudhuri (COMP 507)
UNSW, Carroll Morgan
University of Toronto, Azadeh Farzan
Princeton, Andrew Appel
CMU, Jonathan Aldrich
Chalmers Technical University, Moa Johansson
Eindhoven Technical University, Kees Huizing
Ohio State University, Bruce Weide
Clemson University, Murali Sitaraman
FCT Universidade Nova de Lisboa, Luis Caires
University of the Basque Country, Paqui Lucio
University of Southampton, Michael Butler
- University of Twente, Marieke Huisman
- Yale, Ruzica Piskac
- SUNY Stony Brook, Annie Liu
- University of Edinburgh, Ian Stark (APL14)
- Lübeck University of Applied Sciences, Andreas Schaefer
and tutorials and summer schools:
- Summer School Marktoberdorf, 2008 and 2011
- LASER Summer School, 2011
- Summer School on Logic and Theorem-Proving in Programming Languages, Eugene, OR, 2008
- Tutorial, KTH, Stockholm, 2012
- Invited tutorial, VSTTE 2012
- Tutorial, HILT 2012
- Tutorial, ICSE 2013
If you are, or have been, teaching using Dafny, Rustan Leino would love to know of your experience. And if you want a mention on these lists, please let him know.
- K. Rustan M. Leino and Michał Moskal, Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier, no. MSR-TR-2013-49, 12 July 2013.
- K. Rustan M. Leino, This is Boogie 2, 24 June 2008.