25th Anniversary Distinguished Lecture Series

 

clarkeModel Checking
My 30-year Quest to Overcome the State Explosion Problem

Computer Science Department Turing Centenary Distinguished Lecture
Edmund M. Clarke
FORE Systems Professor of Computer Science, Carnegie Mellon University

Friday, April 27, 11 a.m., TI Auditorium (ECSS 2.102) Refreshments at 10:45 a.m.

 

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 30 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.

Bio
Edmund M. Clarke received a B.A. degree in mathematics from the University of Virginia in 1967, a M.A. degree in mathematics from Duke University in 1968, and a Ph.D. degree in computer science from Cornell in 1976.  He taught at Duke University from 1976-1978 and at Harvard University from 1978-1982. Since 1982 he has been on the faculty in the Computer Science Department at Carnegie-Mellon University. 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.

Dr. Clarke's interests include software and hardware verification and automatic theorem proving. In 1981 he and a graduate student, Allen Emerson, first proposed the use of Model Checking as a verification technique for finite state concurrent systems. His research group pioneered the use of Model Checking for hardware and software verification. In particular, his research group developed Symbolic Model Checking using BDDs, Bounded Model Checking using fast CNF satisfiability solvers, and pioneered the use of CounterExample-Guided-Abstraction-Refinement (CEGAR).  In addition, Clarke and his students developed the first parallel general resolution theorem prover (Parthenon), and the first theorem prover to be based on a symbolic computation system (Analytica).

Dr. Clarke is one of the founders of the conference on Computer Aided Verification (CAV) and served on its steering committee for many years. He is the former editor-in-chief of Formal Methods in Systems Design.  He served on the editorial boards of Distributed Computing, Logic and Computation, and IEEE Transactions in Software Engineering. In 1995 he received a Technical Excellence Award from the Semiconductor Research Corporation. He was a co-recipient of the ACM Kanellakis Award in 1998.  In 1999 he received an Allen Newell Award for Excellence in Research from the Carnegie Mellon Computer Science Department. In 2004 he received the IEEE Harry H. Goode Memorial Award.  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 co-recipient of the 2007 ACM Turing Award for his role in developing Model Checking into a highly effective verification technology, widely adopted in the hardware and software industries. He received the 2008 CADE Herbrand Award for Distinguished Contributions to Automated Reasoning and a 2010 LICS Test-of-Time Award.  In 2011 he was elected to the American Academy of Arts and Sciences.  He received an Honorary Doctorate from the Vienna University of Technology in 2012.  Dr. Clarke is a Fellow of the ACM and the IEEE, and a member of Sigma Xi and Phi Beta Kappa.