Dafny Autumn School

Date: Thursday 8th September and Friday 9th September 2016

Time: 9:30 to 17:00

Venue: Hume Tower, Edinburgh, Teaching Studio LG.07 [room details, access]

Dafny is a verification-aware programming language. Like many other languages, it can be used for writing imperative and functional programs. What sets Dafny apart is that it provides specification constructs that can be used to describe the intended behaviour of programs, and the Dafny environment (in Visual Studio and in Emacs) constantly runs the program verifier in the background to expedite the process of verifying programs. Because of the verifier automation and the streamlined language, Dafny is generally easy to get started with. This has made Dafny a popular tool for teaching concepts of program verification. Dafny was also the language used by the systems projects Ironclad and IronFleet, which with low proof overhead (compared with competing tools) provided high reliability and security.

For when the verifier’s automation is not enough to complete a proof, Dafny includes proof authoring features. These features can be used by themselves, letting users of Dafny give mathematical definitions, define lemmas and write logical proofs, and reason about induction (and co-induction, too). Dafny thus provides the ability to define and prove properties about meta theories, like programming language semantics.

This two-day autumn school will give a working understanding of Dafny through interactive lectures and hands-on exercises. The course will be given by

Rustan Leino (Microsoft Research), who is the architect and main developer of Dafny; and
Gudmund Grov (Heriot-Watt University)

The course will be highly interactive with a combination of presentations with interactive examples and exercises that participants can work on using their laptops. We would recommend that you install Dafny on your laptop (using either the Visual Studio or Emacs IDE) but you can also use it online @ rise4fun. Installation details will be available below in due course.

The course is over two days:

Day 0 (Thursday 8th) will give a introduction to Dafny. Possible topics that may be covered include: Dafny overview: language and tools; simple imperative programs, simple specifications, and interacting with Dafny; simple functional programs, recursion and induction; lemmas, and writing proofs; techniques for debugging verifications; one language: program features vs. proof features.
Day 1 (Friday 9th) will look at more advanced topics. Possible topics include: higher-order functions; mutable data structures; using Dafny to model concurrency; using Dafny to prove meta-theorems about program semantics; tactics for Dafny.

The target audience is (but not restricted to) researchers and doctoral students that want to learn about program verification and Dafny in particular. It is possibly to only attend day 0 if time is a constraint and you are only interested in a basic understanding.

Note that we will be able to adjust the start/end times to allow participants to communte from nearby places,such as Glasgow, Dundee, Stirling, Newcastle, etc

The course is sponsored by EPSRC grant: The Integration and Interaction for Multiple Mathematical Reasoning Processes (EP/N014758/1) and EPSRC grant DTacs - Program Verifier Tactics : Reducing the Development Time for Program Verifiers with re-usable Verification Strategies (EP/M018407/1).

It will be free to attend and lunch and refreshments will be provided...

... but registration will be handled in a first-come-first-served bases with limited spaces available so register now!!!

Registration

Schedule

Thursday 8 September 2016

9:30 - 11:00 : session 1

11:00 - 11:30 : coffee/tea break

11:30 - 13:00 : session 2

13:00 - 13:45 : lunch

13:45 - 15:15 : session 3

15:15 - 15:45 : coffee/tea break

15:45 - 17:00 : session 4

Friday 9 September 2016

9:30 - 11:00 : session 5

11:00 - 11:30 : coffee/tea break

11:30 - 13:00 : session 6

13:00 - 13:45 : lunch

13:45 - 14:30 : session 7

14:30 - 14:45 : coffee/tea break

14:45 - 17:00 : session 8

Tool installation & materials

Dafny can be downloaded from GitHub:

Source code: https://github.com/Microsoft/dafny
Executable for various platforms: https://github.com/Microsoft/dafny/releases

Page updated

Google Sites

Report abuse