Engineering Methods for Ensuring Program Correctness


May 24, 2012


Rustan Leino


Microsoft Research


Common engineering practices today use testing to ensure the quality of software. But relying solely on testing has several well-known drawbacks, such as only testing the program for the given inputs and applying tests only after the entire program has been developed. An idealistic, long-standing dream has been to formally verify the correctness of program, for all inputs. Is there some reality in that dream?

In this talk, I present Dafny, a state-of-the-art tool for program verification. Dafny has been used to verify the full correctness of some challenging algorithms. It was used by two medalist teams in the VSTTE 2012 program verification competition and is being used in teaching. Through demos of this research prototype, I show the vision for how a program verifier can help during software development.


Rustan Leino

Rustan Leino is a principal researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond. He is a 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. Rustan is the architect of the Boogie program verification framework, which underlies more than a dozen program verifiers for C, Spec#, and other languages. Before earning his PhD from Caltech in 1995, Rustan designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. He collects thinking puzzles on a popular webpage and has started the Verification Corner video blog on