Patrice Godefroid

(Microsoft Research)

"Software Model Checking 2.0"

(Vortrag im Rahmen der "Distinguished Lecture Series 07/08" des Max Planck Instituts für Software-Systeme)

About 25 years ago, a new verification paradigm named "model checking" was introduced whereby checking whether a program satisfies a property is done by systematically exploring the program's state space. Since then, model checking has been much discussed in research circles and is viewed as very successful by most academic standards (high citation counts, 2008 Turing Award, etc.). Yet, model checking applied to software is still in its infancy. A first generation of model checkers for finite-state software designs, like SPIN and SMV, where engineered in the 90's. The last decade saw a second generation of software model checkers, like VeriSoft and SLAM, directly applicable to programming languages, such as C, and effective for specific application domains, namely communication protocols and device drivers, respectively.

I will argue that a third generation of general-purpose software model checkers is currently emerging. Their foundation is systematic testing. They combine program analysis, testing, model checking and theorem proving. And their "killer app" is security, which makes the improbable corner cases typically found by model checking suddently relevant when they can be triggered by an attacker. This transition is happening at Microsoft where, for the first time, software model checking (albeit still in a weak form) is starting to be deployed on a larger scale for a wide range of data-driven applications. I will talk about these latest developments.