Department of Computer Science at RPTU in Kaiserslautern

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.

Patrice Godefroid

Patrice Godefroid is a Principal Researcher at Microsoft Research. He received the B.S. degree in Electrical Engineering (Computer Science elective) and the Ph.D. degree in Computer Science from the University of Liege, Belgium, in 1989 and 1994 respectively. From 1994 to 2006, he worked at Bell Laboratories (part of Lucent Technologies), where he was promoted to "distinguished member of technical staff" in 2001. His research interests include program (mostly software) specification, analysis, testing and verification.

Zeit: Freitag, 04. April 2008, 16:00 Uhr
Ort: TU Kaiserslautern, Gebäude 42, Raum 110
Hinweis: Der Vortrag wird live an die Universität des Saarlandes MPI-Gebäude E1.4 Raum 019 übertragen.