Engineering Methods for Ensuring Program Correctness

Speaker  Rustan Leino

Affiliation  Microsoft Research

Host  Jaime Puente

Duration  00:52:41

Date recorded  24 May 2012

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.

©2012 Microsoft Corporation. All rights reserved.
Learn more
> Engineering Methods for Ensuring Program Correctness