*** Dafny mini-course ***

Theorem Proving and Program Verification with Dafny

Rustan Leino has kindly agreed to run a 3 half-day tutorial on Dafny, its use for functional and for imperative programs, and its implementation.

Wednesday, 26.03,  Imperial College, William Penny, room 301
          12:00 – 13:00
          16:00 – 17:30
Thursday, 27.03,   Imperial College, William Penny, room 301
          13:30 – 17:00
Friday, 28.03, Imperial College, Huxley, room 345
          11:00 – 13:00
           14:00 – 17:00

Participation open to all. Lots of interaction encouraged. For any queries, email Sophia Drossopoulou.

Details: Dafny is a programming language designed for reasoning.  In this mini-course, I will teach the basic use of Dafny, leading up to the proofs of some interesting imperative programs as well as the formalization of a little program semantics.  The goal is that participants will become familiar enough with Dafny that they can comfortably use it to prove their next algorithm, confirm their next hallway-discussion proof, or write their next POPL paper with Dafny.  On the way, we will see recursive functions, lemmas, proof calculations, and a lot of induction.

Dafny can be run in a web browser at rise4fun.com/Dafny.  The best interactive experience is obtained using the Dafny IDE; if you have Visual Studio, install the Dafny IDE from here.  You can also install a command line version of Dafny.

Here are a few useful papers and links that may be of interest before, during, or after the mini-course:

  • “Developing Verified Programs with Dafny” (3 pages), K. Rustan M. Leino, tutorial notes, ICSE 2013 [PDF]
  • “Getting Started with Dafny: A Guide”, Jason Koenig and K. Rustan M. Leino, Marktoberdorf 2011 lecture notes, [PDF] [rise4fun online tutorial]
  • “Verified calculations”, K. Rustan M. Leino and Nadia Polikarpova, VSTTE 2013 [PDF]
  • “Automating Theorem Proving with SMT”, K. Rustan M. Leino, ITP 2013 [PDF]
  • “How to write your next POPL paper in Dafny”, Nada Amin [video]
  • “Writing inductive proofs about programs that operate on trees”, Sophia Drossopoulou and K. Rustan M. Leino, Verification Corner [video]

Short Bio: Rustan is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research and Visiting Professor in the Department of Computing at Imperial College London.  His research interests include a focus on programming tools, both mental and mechanical.