![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > Developing verified programs in Dafny
Developing verified programs in DafnyAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsFaculty of Divinity Gates Cambridge Annual Lecture 7 March 2017 Cambridge Centre for Political ThoughtOther talksMicrosporidia: diverse, opportunistic and pervasive pathogens Random Feature Expansions for Deep Gaussian Processes Modelling discontinuities in simulator output using Voronoi tessellations Grammar Variational Autoencoder Magnetic Resonance on Two Scales for Research into Cell Cycle and Stroke Future directions panel |