Dafny is an auto-active program verifier for an imperative language with functional and object oriented features that uses the Boogie intermediate verification language and the Z3 SMT solver for automated proof.
This is one of the early papers about Dafny: before it could actually execute the code it verifies. (I am reminded of the Donald Knuth comment about a function that it had been verified but not actually executed.) It also describes the origins of Dafny as an exploration of dynamic frames and some of the development of features driven by features of the code they wanted to verify.
The main body of the paper is a description of the language feature and how it is converted to Boogie – with some of the author’s characteristic asides about how the choices impact verification and where the ideas were first explored. (I really like this feature of Leino’s papers.)
The big result in the paper is a verified version of the Schorr-Waite algorithm in just 117 lines of code, proof and comment. Wow! Also a nice summary of the development process. The only thing not to like about this is the 19 loop invariants required. (I wonder whether loop specifications in the style of Tuerk would help at all?) Also, the author admits that “deciphering the verifier’s error messages” is hard. I wonder how much that improved in later versions or with the development of the Boogie Verification Debugger?
Papers related to Dafny: An automatic program verifier for functional correctness
- Komodo: Using verification to disentangle secure-enclave hardware from software [ferraiuolo:sosp:2017]
- The Boogie verification debugger [legoues:sefm:2011]
- Developing verified programs with Dafny [leino:icse:2013]
- Verifying security invariants in ExpressOS [mai:asplos:2013]