Harnessing SMT power using the verification engine Boogie

SMT solvers provide decision-procedure power to a large number of practical problems. When those problems are related to program analysis or program verification, the input language of SMT solvers is too far removed. Instead, an intermediate verification language (like Boogie or Why) gives a suitable level of abstraction to describe the problems to be solved. Such a language offers a mix of mathematical features and program-oriented imperative features. In this talk, I show through examples how one benefits from using Boogie in encoding program-related problems.

Rustan Leino, Microsoft Research, Redmond, USA

K. Rustan M. Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research in Redmond, WA, USA. He is a world leader in building automatic program verifiers and is generally known for his work on programming methods and program verification tools. He has used SMT solvers for over 15 years, starting when he worked on specifications on the pioneering ESC/Modula-3 project at the DEC Systems Research Center (SRC).  Since then, he has led a number of programming language and verification projects, including the extended static checker ESC/Java (at Compaq SRC), and (at Microsoft Research) Spec# (which provided enforced pre- and post-conditions on the .NET platform and has led to the Code Contracts in .NET 4.0), Chalice (which explores the specification and static verification of concurrent programs), and Dafny (which has advanced the boundaries of using automatic SMT solving to do functional-correctness verification of programs). He is the architect of the Boogie program verification framework, which underlies more than a dozen program verifiers for C, Spec#, and other languages.

Before getting his PhD (Caltech, 1995), Leino 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 has recently started the Verification Corner video show on channel9.msdn.com. In his spare time, he plays music and teaches cardio exercise classes.