Developing verified programs in Dafny

Add to your list(s) Download to your calendar using vCal

• Rustan Leino
• Monday 27 February 2012, 12:45-14:00
• FW26.

If you have a question about this talk, please contact Peter Sewell.

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.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory talks
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.