Speaker: Edmund M. Clarke
Professor, School of Computer Science and Department of Electrical and Computer Engineering
Carnegie Mellon University
Title: My 28-year Quest to Overcome the State Explosion Problem
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.
Specifications are written in temporal logic,
which is particularly valuable for expressing concurrency properties.
An intelligent, exhaustive search is used to
determine if the specification is true or not. If the specification is not
true, the Model Checker will produce a counterexample execution trace that
shows why the specification does not hold. This feature is extremely useful for
finding obscure errors in complex systems. The main disadvantage of Model
Checking is the state-explosion problem, which can occur if the system under
verification has many processes or complex data structures. Although the
state-explosion problem is inevitable in worst case, over the past 27 years
considerable progress has been made on the 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: Clarke’s interests include software and hardware verification and automatic theorem proving. His research group pioneered the use of Model Checking for hardware verification, developed Symbolic Model Checking using BDDs, and developed the first parallel resolution theorem prover (Parthenon) and the first theorem prover to be based on a symbolic computation system (Analytica). Among other awards, Clarke was a recipient of the 2007 ACM Turing Award (with Allen Emerson and Joseph Sifakis) for his role in developing Model Checking into a highly effective verification
technology, widely adopted in the hardware and software industries.
See more information on the DCS DLS
here.