Electrical and Computer Engineering at Carnegie Mellon University

Edmund Clarke Jr.

FORE Systems Professor – CS ; Professor – ECE

Department	Electrical and Computer Engineering
Office	9231 Gates-Hillman Center
Telephone	(412)-268-2628
Fax	(412)-268-5576
Email	edmund.clarke@cs.cmu.edu
Assistant	Denny Marous

Research Interests

Logical errors in sequential circuit designs and protocols are an important problem for hardware designers. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. Professor Clarke's 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 last few years, 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), he has been able to check some examples that would have required 10<sup>2</sup> states with the original algorithm. Various refinements of the BDD-based techniques have pushed the state count up to 10<sup>100</sup>. By combining model checking with various abstraction techniques, he has been able to handle even larger systems. For example, he has used this technique to verify the cache coherence protocol in the IEEE Futurebus+ Standard. He 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.