# Ed Clarke

- DIMACS Center - Rutgers University
- CoRE Building, 1st Floor Lecture Hall
- Piscataway, New Jersey
- Friday, March 22, 1996
- 11:00 AM

## Topic of Discussion

MODEL CHECKING AND SYMMETRY
## Abstract:

Model checking is an automatic technique for verifying finite-state
reactive systems, such as sequential circuit designs and communication
protocols. Specifications are expressed in temporal logic, and the
reactive system is modeled as a state-transition graph. An efficient
search procedure is used to determine whether or not the
state-transition graph satisfies the specifications.
In practice, reactive systems often exhibit considerable symmetry. We
investigate techniques for reducing the complexity of model checking
in the presence of symmetry. In the past, symmetry has been exploited
in computing the set of reachable states of a system when the
transition relation is represented explicitly. In this talk, we show
how to handle arbitrary temporal properties and various complications
that arise when binary decision diagrams are used.

## About the Speaker:

Edmund M. Clarke is an acknowledged leader in the field of software
and hardware verification. Dr. Clarke has degrees in mathematics
>from the University of Virginia and from Duke University, and received
his Ph.D. degree in Computer Science from Cornell University 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. His interests include software and hardware verification and
automatic theorem proving.

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 two
international conferences, Logic in Computer Science and Computer-Aided
Verification. He is a member of the Association
for Computing Machinery, IEEE Computer Society, Sigma Xi, and Phi Beta
Kappa.

Remaining speakers in the Distinguished Lecturer Series of the
DIMACS Special Year on Logic and Algorithms are:

- Vaughn Pratt (Stanford University),
- Alexander Razborov (Steklov Mathematical Institute).

For additional information about the DIMACS special year, please see the
following web site:
- http://dimacs.rutgers.edu/SpecialYears/1995_1996/

dimacs-www@dimacs.rutgers.edu
Document last modified on March 8, 1996