Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
Software Model Checking 2.0
Patrice Godefroid
Microsoft Research
SWS Distinguished Lecture Series - Spring
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.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 4 April 2008
16:00
60 Minutes
42
110
University Kaiserslautern
Abstract
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.
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.
Contact
Brigitta Hansen
0681 - 9325200
--email hidden
Video Broadcast
Yes
MPI SWS Saarbruecken
E 1 4
019
passcode not visible
logged in users only
Carina Schmitt, 04/07/2008 16:15
Uwe Brahm, 04/04/2008 12:12
Carina Schmitt, 04/03/2008 20:25
Brigitta Hansen, 04/01/2008 12:09
Brigitta Hansen, 03/31/2008 14:16
Brigitta Hansen, 03/20/2008 16:55 -- Created document.
Uwe Brahm, 04/04/2008 12:12
Carina Schmitt, 04/03/2008 20:25
Brigitta Hansen, 04/01/2008 12:09
Brigitta Hansen, 03/31/2008 14:16
Brigitta Hansen, 03/20/2008 16:55 -- Created document.