By Rustan Leino, Microsoft Research, Redmond, USA.
The practice of using formal program verification in everyday software engineering has long been a dream. But it hasn't come into fruition. Will it ever? Or has it already? In this talk, I will, from a personal perspective, highlight some scientific milestones that have enabled us to build verifiers today. I will then do a brief overview of some verification tools in use at Microsoft today, as well as show a technological frontier of what tools are capable of doing today, which might impact education. Finally, I will sketch some trends and directions for future research.
Rustan 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.
This article was published on Mar 21, 2011