Edmund Clarke
FORE Systems Professor – CS; Professor – ECE
| Contact Information | |
|---|---|
| Department | Computer Science |
| Office | 7117 Wean Hall |
| Telephone | (412)-268-2628 |
| Fax | (412)-268-5574 |
| emc@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 102 states with the original algorithm. Various refinements of the BDD-based techniques have pushed the state count up to 10100. 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.
In the News
- Clarke Elected to Academy of Arts & Sciences
- Clarke Wins Computing's Highest Honor
- Clarke Receives Top Citations on Microsoft Libra
- ECE Graduate Students Win Best in Session Awards
- ECE Faculty Among Most Cited in IEEE Transactions on Computer-Aided Design
- Clarke Elected to National Academy of Engineering
- Edmund Clarke Elected IEEE Fellow
- CSSI Participates in DAC; Hosts Alumni & Friends Reception
- Bryant Named New School of Computer Science Dean
- Clarke Wins IEEE's Harry M. Goode Memorial Award
- Clarke One of Two CMU Professors Featured in ComputerWorld
- CMU Faculty Awarded More Than $24 Million in Grants From NSF's ITR Initiative
- Several Faculty in ECE and Computer Science Awarded DOD Grants
Keywords
Hardware and software verification, automatic theorem proving, symbolic computation
Education
PhD, 1976
Computer Science
Cornell University
MS, 1974
Computer Science
Cornell University
MA, 1968
Mathematics
Duke University
BA, 1967
Mathematics
University of Virginia