Department of  Computing

Applications of Computing in Industry : Lecture

18 February
12pm, LT308 Huxley
company: Imperial College London

Title: Introduction to Dafny

Dafny is a tool developed at Miscrosoft Research for the verification of imperative as well as functional programs.

We shall introduce the imperative features of Dafny, the pre- and post-conditions to methods, show some examples where Dafny can infer correctness of the program unaided, and other examples, where it needs some "hints".

More information at
The tool can be tried out online at

Speaker Details: Sophia Drossopoulou

Professor of Programming Languages

Social Bookmarking: