February 23, 2005
Edmund M. Clarke has been elected to the National Academy of Engineering (NAE). Clarke is Carnegie Mellon University's FORE Systems Professor of Computer Science and a professor of Electrical and Computer Engineering.
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 10,100 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 the verification of circuit designs.
Clarke earned a B.A. and M.A. in mathematics from the University of Virginia and Duke University, respectively. He then received both an M.S. and Ph.D. 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 of the Association for Computing Machinery's Kanellakis Award for the development of Symbolic Model Checking, along with Randal Bryant, dean of the Carnegie Mellon School of Computer Science, Allen Emerson, and Kenneth McMillan. 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 and the IEEE, as well as a member of 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. Aaronson, Alfred Blumstein, Randal E. Bryant, Robert F. Davis, *Steven J. Fenves, Richard J. Fruehan, Ignacio E. Grossman, *Angel G. Jordan, Takeo Kanade, Mark H. Kryder, *Harold W. Paxton, Raj Reddy, *Ronald A. Rohrer, Daniel P. Siewiorek, *Herbert L. Toor, *Arthur W. Westerberg and *Robert M. White.
Source: Jenni King, Carnegie Mellon Today