• Created by Unknown User (leberre_1@touchstonenetwork.net), last modified on Jun 14, 2011 04:59

You are viewing an old version of this page. View the current version.

Compare with Current View Page History

« Previous Version 2 Next »

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. At Microsoft Research, he has led a number of programming language and verification projects, including 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. Previously, Leino led the ESC/Java project at the Compaq Systems Research Center (SRC) and worked on specifications on the pioneering ESC/Modula-3 project at DEC SRC.
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.

  • No labels