Rustan Leino
Microsoft Research - Resesrch in Software Engineering (RiSE)

Induction, Co-induction, Calculations - What's Not to Like About Dafny?

There was a time when formal proofs of program correctness were best done with interactive theoerm provers. The automation offered by modern SMT solvers has changed the landscape in favor of auto-active program verifiers.

There was a time when formal proofs of theorems about semantics and mathematics were best done with interactive theorem provers. This is still true today. Meanwhile, today also shows the emergence of the first SMT-based tools for doing such proofs.

In this talk, I will show the support for proving theorems in Dafny, an auto-active program verifier. In particular, I will show Dafny's support for induction, co-induction and calculations. Although currently limited to a first-order setting, the proofs that can be performed using Dafny show a comprehensive degree of automation. Might the landscape for formal theorem proving be changing?

Joint work with Michal Moskal and Nadia Polikarpova, with contributions by Nada Amin and Valentin Wustholz.
Dafny homepage:

Rustan Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond. He is known for his work on programming methods and program verification tools. These include the langiages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3. With Dafny, Leino has pushed the boundaries of what can be done with an auto-active SMT-based program verifier. With Dafny's proof features, he is pushing the boundaries of his own understanding.

Prior to Microsoft Research, Leino worked at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner video show on In his spare time, he plays music and recently having ended his tenure as cardio exercise class instructor, is trying to learn to dance.


Host: Jonathan Aldrich

Friday, November 16, 2012
2:30 p.m.
Gates & Hillman Center - 8102

Principles of Programming Seminars