Induction, co-induction, calculations — what’s not to like about Dafny?
ABSTRACT:
There was a time when formal proofs of program correctness were best done with interactive theorem provers. The automation offered by modern SMT solvers has since 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 competitive degree of automation. Might the landscape for formal theorem proving be changing? Joint work with Michał Moskal and Nadia Polikarpova, with contributions by Nada Amin and Valentin Wüstholz. Dafny homepage: http://research.microsoft.com/dafny
SPEAKER AND BIO:
K. Rustan M. Leino (http://research.microsoft.com/~leino), Microsfot Research
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 languages 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 channel9.msdn.comb http://channel9.msdn.com. In his spare time, he plays music and, recently having ended his tenure as cardio exercise class instructor, is trying to learn to dance.