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.