Well-founded functions, induction, and extreme predicates in an SMT-based verifier

by Rustan Leino

Abstract
An SMT solver takes first-order formulas as input and provides impressive automation.  But what if the problem at hand goes beyond first order?  The Dafny program verifier provides well-founded functions, inductive proofs, and predicates defined as least and greatest fixpoints.  It encodes properties of these into first-order logic in such a way that harnesses the automation of SMT solvers.  In this talk, I will give an overview of functions and induction in Dafny, and will then focus on the encoding on predicates defined by fixpoints.

Bio
Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. He is known for his work on programming methods and program verification tools, and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.  He is an ACM Fellow.
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 channel on youtube. In his spare time, he likes to cook and, being a multi-instrumentalist, play music. Leino instructed group cardio and strength classes for many years, he more recently danced on a salsa performance team, and he once needed a helicopter to get off a Swiss mountain.

More information