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/

Index

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