The increasing role of verification in software development

Abstract: Formal verification has been applied to hardware and communication protocols for some time.  Does verification also have a place for software in general?  Microsoft routinely makes use of a number of tools based on verification technology, providing a fine-grained comb that searches for certain kinds of errors.  As tools become better and more acceptable, future developers may be able to use them while writing and maintaining software.  In this talk, I will give a taste of some tools that are being applied to software at Microsoft and will show a prototype of how formal verification can assist developers more directly.

Biography: Rustan Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research. 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 led a number of programming language and verification projects, including Spec# (which extends C# with contracts and was a forerunner of the Code Contracts in Microsoft .NET 4.0), Chalice (for concurrent programs), Dafny (for functional-correctness verification), and, previously, ESC/Java. 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 Ph.D. (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 webpage and has started the Verification Corner video blog on channel9.msdn.com. In his spare time, he plays music and teaches cardio exercise classes.

Rustan Leino's Homepage