Applications of Computing in Industry : Lecture

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 http://research.microsoft.com/en-us/projects/dafny/
The tool can be tried out online at http://rise4fun.com/dafny

Professor of Programming Languages