Early Verification

echnology that accurately models, analyzes, and verifies software has come a long way since its conception several decades ago.  One mode of using such technology is to look for defects in software that has already left the hands of developers.  Another mode is to integrate the technology into the process of software authoring.  The advantage of this mode is that it lends analytical power to the developer's thinking.  To be used in this way, the technology must be packaged in a way that is understandable, unobtrusive, and responsive.

In this talk, I showcase an integrated development environment that supports reasoning and verification, trying to provide an aid to the developer earlier during the software development process.

Bio: Prof. Dr. K. Rustan M. Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research and a Visiting Professor in the Computing Department at Imperial College London.  He is known for his work on programming methods, languages, and verification, and is a world leader in building automated program verification tools.  Languages and tools he has worked on include Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.  In the past, he has worked as a researcher at DEC and Compaq, and as a software engineer at Microsoft.  He received his PhD in Computer Science from Caltech in 1995.

Leino also collects thinking puzzles on a popular web page and hosts the Verification Corner channel on youtube.  In his spare time, he enjoys playing music, cooking food, and, having ended a 7-year tenure as group cardio exercise instructor, learning to dance.