Rustan Leino Microsoft Research - Resesrch in Software Engineering (RiSE)
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 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: http://research.microsoft.com/dafny Bio: 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 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.