Edmund Melson Clarke, Jr. (July 27, 1945 – December 22, 2020) was an American computer scientist and teacher known for creating model checking, a method used to check if hardware and software work correctly. He held the title of FORE Systems Professor of Computer Science at Carnegie Mellon University. Clarke, along with E. Allen Emerson and Joseph Sifakis, won the 2007 ACM Turing Award.

Biography

Clarke was born in Newport News, Virginia. He earned a B.A. degree in mathematics from the University of Virginia in Charlottesville in 1967. He received an M.A. degree in mathematics from Duke University in Durham, North Carolina, in 1968. In 1976, he completed a Ph.D. degree in computer science from Cornell University in Ithaca, New York. After earning his Ph.D., he taught in the Department of Computer Science at Duke University for two years. In 1978, he moved to Harvard University in Cambridge, Massachusetts, where he worked as an assistant professor of computer science in the Division of Applied Sciences. He left Harvard in 1982 to join the faculty in the Computer Science Department at Carnegie Mellon University in Pittsburgh, Pennsylvania. He was named a full professor in 1989. In 1995, he became the first person to receive the FORE Systems Professorship, a special position in the Carnegie Mellon School of Computer Science. In 2008, he was appointed a university professor, and in 2015, he became an emeritus professor. Clarke died from COVID-19 in December 2020 at the age of 75 during the pandemic in Pennsylvania.

Work

Clarke was interested in checking the correctness of software and hardware, as well as using computers to prove mathematical theorems. In his Ph.D. thesis, he showed that some control structures in programming languages did not work well with Hoare-style proof systems. In 1981, he and his student E. Allen Emerson suggested using model checking to verify systems with limited states that operate simultaneously. His research team was among the first to use model checking to check hardware designs. His group also created symbolic model checking using a type of diagram called binary decision diagrams. This technique became the focus of Kenneth L. McMillan's Ph.D. thesis, which won an ACM Doctoral Dissertation Award. Additionally, his team created the first parallel resolution theorem prover called Parthenon and another theorem prover named Analytica, which used symbolic computation. In 2009, he helped start the Computational Modeling and Analysis of Complex Systems (CMACS) center, which was supported by the National Science Foundation. This center brings together researchers from several universities to use abstract interpretation and model checking in biological and embedded systems.

Professional recognition

Clarke was a member of the ACM and the IEEE. He received an award for technical excellence from the Semiconductor Research Corporation in 1995 and an Allen Newell Award for research excellence from the Carnegie Mellon Computer Science Department in 1999. He shared the ACM Paris Kanellakis Award in 1999 with Randal Bryant, Emerson, and McMillan for creating symbolic model checking. In 2004, he received the IEEE Computer Society Harry H. Goode Memorial Award for important and groundbreaking work in verifying the correctness of hardware and software systems and for the great influence this work had on the electronics industry. He was elected to the National Academy of Engineering in 2005 for contributions to verifying the correctness of hardware and software. He was elected to the American Academy of Arts and Sciences in 2011. He received the Herbrand Award in 2008 for his role in inventing model checking and for his long-term leadership in this field. In 2012, he received an honorary doctorate from TU Wien for his outstanding contributions to informatics. He received the 2014 Bower Award and Prize for Achievement in Science from the Franklin Institute for his key role in creating and developing techniques to automatically verify the correctness of computer systems used in transportation, communications, and medicine. He was a member of Sigma Xi and Phi Beta Kappa.