[10-16]Model Checking: My 28-year Quest to Overcome the State Explosion Problem

Date:2009-10-12

Title：Model Checking: My 28-year Quest to Overcome the State Explosion Problem
Speaker：Edmund M. Clarke （Computer Science Department，Carnegie Mellon University）
Time：10:00 — 11:00 am, Friday, October 16
Venue：Lecture room, Level 3 Building #5, State Key Lab of Computer Science

Abstract：
Model Checking is an automatic verification technique for state-transition systems that are finite-state or that have finite-state abstractions. In the early 1980’s in a series of joint papers with my graduate students E.A. Emerson and A.P. Sistla, we proposed that Model Checking could be used for verifying concurrent systems and gave algorithms for this purpose. At roughly the same time, Joseph Sifakis and his student J.P. Queille at the University of Grenoble independently developed a similar technique. Model Checking has been used successfully to reason about computer hardware and communication protocols and is beginning to be used for verifying computer software. By expressing a system’s specifications in temporal logic, the Model Checker can perform an exhaustive search to determine if the specification is true. In those cases where the specification does not hold, the Model Checker produces a counterexample execution trace. We have found this feature to be extremely useful for finding obscure errors in complex systems. However, Model Checking is vulnerable to the state-explosion problem, which can occur if the system being verified has many processes that execute in parallel or complex data structures. In some cases, the state-explosion problem is inevitable, but over the past 27 years we have made considerable progress in overcoming this problem for certain classes of state-transition systems that occur often in practice. In this talk, I will describe what Model Checking is, how it works, and the main techniques that have been developed for combating the state-explosion problem.

Biography：
Edmund M. Clarke received a Ph.D. degree in Computer Science from Cornell University, Ithaca NY, in 1976. He joined the faculty in the Computer Science Department at Carnegie-Mellon University, Pittsburgh, PA in 1982. He was appointed Full Professor in 1989. In 1995 he became the first recipient of the FORE Systems Professorship, an endowed chair in the School of Computer Science. He was named a University Professor in 2008.
Prof. Clarke’s research interests include software and hardware verification and automatic theorem proving. In 2004 he received the IEEE Harry H. Goode Memorial Award for significant and pioneering contributions to formal verification of hardware and software systems, and for the profound impact these contributions have had on the electronics industry. He was elected to the National Academy of Engineering in 2005 for contributions to the formal verification of hardware and software correctness. He was a recipient with Allen Emerson and Joseph Sifakis of the 2007 ACM Turing Award Model Checking into a highly effective verification technology, widely adopted in the hardware and software industries.