Edmund Clarke Jr.

FORE Systems Professor – CS Courtesy Professor – ECE
Office 9231 Gates-Hillman Center
Telephone (412)-268-2628
Fax (412)-268-5576
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.

In the News

  • Chinese Academy of Sciences Honors Clarke
  • 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
  • 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
  •  Edmund  Clarke Jr.

    Research Area



    Hardware and software verification, automatic theorem proving, symbolic computation


    PhD, 1976
    Computer Science
    Cornell University

    MS, 1974
    Computer Science
    Cornell University

    MA, 1968
    Duke University

    BA, 1967
    University of Virginia