Rustan Leino, Microsoft Research - Program Verification: Yesterday, Today, Tomorrow

Informatics presents a series of distinguished lectures which aims to present excellent speakers describing intriguing topics in an engaging style.

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.

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.

Category:

Science & Technology

Tags:

• program
• verification
• software
• engineering
• tools
• microsoft
• automatic
• methods
• research
• trends

[felpaluche]

Wow!  Remarkable wrap-up!

[henkvanderlaak]

So.... the obvious question is: Why don't they use it for their own products?

I hold Microsoft responsible for the current attitude of the general public, that it "is just a fact of live" that your software breaks down on a daily basis. The credibility of this talk is zero. Sorry, but it had to be said.