Computer Science Professor Elected to National Academy of Engineering
Carnegie Mellon Today

Carnegie Mellon Today

Carnegie Mellon News Services Home Page

Computer Science Professor Elected to National Academy of Engineering

Computer Science Professor Edmund Clarke was elected to the NAE for his contributions to the formal verification of hardware and software correctness.
Edmund M. Clarke, Carnegie Mellon University's Fore Systems Professor of Computer Science, has been elected to the National Academy of Engineering (NAE).

Membership in the NAE honors people who have made important contributions to engineering theory and practice and who have demonstrated unusual accomplishments in pioneering new and developing fields of technology. It is one of the highest professional distinctions an engineer can achieve.

Established in 1964, the NAE shares responsibility with the National Academy of Sciences to advise the federal government on questions of policy in science and technology.

Clarke was elected to the academy for his contributions to the formal verification of hardware and software correctness. He developed technology that reduces the number of errors in digital circuit designs, a problem that has become more significant than manufacturing difficulties in bringing new computer products to market.

His technique, called model checking, which he developed with several students, is superior to simulation, the only other technique available to detect flaws in computer circuits. Model checking searches all possible states of a circuit to determine if its behavior satisfies a specification in a specialized notation called temporal logic, a language for making statements about the behavior of a system over time. Coupling temporal logic formulas and a specialized data structure called a binary decision diagram, Clarke and his colleagues have been able to search and find errors in circuits with as many as 10100 states.

Since Clarke began developing model checking in 1981, companies including AT&T Bell Labs, Intel Corp., Hewlett Packard Co., Bull S.A., Siemens A.G., Fujitsu Ltd., Motorola Inc., IBM Corp., and groups at universities around the world have been investigating and using model checking to improve verification of circuit designs.

Clarke holds a bachelor's degree in mathematics from the University of Virginia. He received both his master's and doctor's degrees in computer science from Cornell University.

Before joining the Carnegie Mellon faculty in 1982, Clarke taught in Duke University's Department of Computer Science and Harvard University's Division of Application Sciences.

In 1999, Clarke was a co-winner, along with Carnegie Mellon School of Computer Science Dean Randy Bryant, Allen Emerson, and Kenneth McMillan, of the Association for Computing Machinery's Kanellakis Award for the development of Symbolic Model Checking. For this work he also received a Technical Excellence Award from the Semiconductor Research Corporation in 1995 and an Allen Newell Award for Excellence in Research from the Carnegie Mellon Computer Science Department in 1999.

Clarke has served on the editorial boards of "Distributed Computing" and "Logic and Computation" and is currently on the editorial board of IEEE Transactions in Software Engineering. He is a former 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.

Clarke is a fellow of the Association for Computing Machinery, the IEEE Computer Society, Sigma Xi, and Phi Beta Kappa. In 2004, he received IEEE's Harry H. Goode Memorial Award, which recognizes outstanding achievements in the information processing field.

Clarke joins a distinguished list of Carnegie Mellon faculty who are members of the NAE. Others include Hubert I. Aarenson, David H. Archer, Alfred Blumstein, Randal Bryant, Robert F. Davis, Richard J. Fruehan, Ignacio Grossman, Angel G. Jordan, Takeo Kanade, Harold W. Paxton, Raj Reddy, Daniel P. Siewiorek, Herbert L. Toor, Arthur W.Westerberg and Robert M. White.

Jenni King

Carnegie Mellon Home