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