"Symbolic Model Checking with and without BDDs"
Dr.
Edmund Clarke
FORE Systems Professor of Computer Science
Carnegie Mellon University
Thursday, April 20
Abstract:
Logical errors in finite-state concurrent systems such as sequential
circuit designs and communication protocols are an important problem
for computer scientists. They can delay getting a new product on the
market or cause the failure of some critical device that is already in
use. My research group has developed a verification method called
temporal logic model checking for this class of systems. In this
approach specifications are expressed in a propositional temporal
logic, while circuits and protocols are modeled as state--transition
systems. An efficient search procedure is used to determine
automatically if a specification is satisfied by some transition
system. The technique has been used in the past to find subtle errors
in a number of non-trivial examples.
During the past decade, the size of the state-transition systems
that can be verified by model checking techniques has increased
dramatically. By representing transition relations implicitly using
Binary Decision Diagrams (BDDs), we have been able to check some
examples that would have required states with the original
algorithm. Various refinements of the BDD-based techniques have
pushed the state count up to .
By combining model checking
with various abstraction techniques, we have been able to handle even
larger systems. For example, we have used this technique to verify the
cache coherence protocol in the IEEE Futurebus+ Standard. We found
several errors that had been previously undetected. Apparently, this
is the first time that formal methods have been used to find
nontrivial errors in an IEEE standard.
Although we believe that model checking is already useful for
verifying many circuit and protocol designs that arise in industry,
additional research is needed to exploit the full power of this
method. We have recently developed a new technique called {\em
bounded model checking} that uses fast propositional decision
procedures like Stahlmarck's algorithm instead of BDDs to handle even
larger examples. We have evaluated the new technique by verifying
twenty one complex circuits from the Power PC Microprocessor.
Traditional model checking techniques based on BDDs were only
able to handle one of the circuits we tried.
Biography:
Edmund M. Clarke received a B.A. degree in mathematics from the
University of Virginia, Charlottesville, VA, in 1967, an M.A. degree
in mathematics from Duke University, Durham NC, in 1968, and a Ph.D.
degree in Computer Science from Cornell University, Ithaca NY, in
1976.
After receiving his Ph.D., he taught in the Department of Computer
Science, Duke University, for two years. In 1978 he moved to Harvard
University, Cambridge, MA where he was an Assistant Professor of
Computer Science in the Division of Applied Sciences. He left Harvard
in 1982 to join the faculty in the Computer Science Department at
Carnegie-Mellon University, Pittsburgh, PA. 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.
Dr. Clarke's interests include software and hardware verification and
automatic theorem proving. In his Ph.D. thesis he proved that certain
programming language control structures did not have good Hoare style
proof systems. In 1981 he and his Ph.D. 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 verification. Symbolic Model
Checking using BDDs was also developed by his group. This important
technique was the subject of Kenneth McMillan's Ph.D. thesis, which
received an ACM Doctoral Dissertation Award. In addition, his resarch
group developed the first parallel resolution theorem prover
(Parthenon) and the first theorem prover to be based on a symbolic
computation system (Analytica).
Dr. Clarke has served on the editorial boards of Distributed Computing
and Logic and Computation and is currently an editor-in-chief of
Formal Methods in Systems Design. He is on the steering committees of
Logic in Computer Science and
Computer-Aided Verification. He was a cowinner along with Randy
Bryant, Allen Emerson, and Kenneth McMillan of the ACM Kanellakis
Award in 1999 for the development of Symbolic Model Checking. For this
work he also received a Technical Excellence Award from the
Semiconductor Research Corporation in 1995 and an Allen Newell Award
for Excellence in Research from the Carnegie Mellon Computer Science
Department in 1999. Dr. Clarke is a Fellow of the Association for
Computing Machinery, a member of the IEEE Computer Society, Sigma Xi,
and Phi Beta Kappa.
Recept: 3:30-4 p.m.
Talk: 4-5:00 p.m.
Room 2135,
Engineering
Building
Host: K. Stirewalt