Abstract

Dafny is a programming language and program verifier. The language is sequential and includes common imperative features, dynamic object allocation, and inductive datatypes. It also includes specification constructs like pre- and postconditions. Because the Dafny verifier runs continuously in the background, the consistency of a program and its specifications is always enforced.

Dafny has been used to verify a number of challenging algorithms, including Schorr-Waite graph marking, Floyd’s “tortoise and hare” cycle-detection algorithm, and snapshotable trees with iterators. Dafny is also being used in teaching and it was a popular choice in the VSTTE 2012 program verification competition (where two of the Dafny teams received medals). Its open-source implementation (which rests on Boogie and makes use of the SMT solver Z3) has also been used as a foundation for other verification tools.

In this talk, I will give a taste of how to use Dafny to write correct code. In addition to showing the basic interaction with Dafny (which is done via the program text), I will show how to debug verification attempts and how to formulate and prove (often inductive) lemmas.