Patrice Godefroid(Microsoft Research)
"Software Model Checking 2.0"
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 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.|