University of Cambridge > > Semantics Lunch (Computer Laboratory) > Developing verified programs in Dafny

Developing verified programs in Dafny

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity