 | This article includes a list ofgeneral references, butit lacks sufficient correspondinginline citations. Please help toimprove this article byintroducing more precise citations.(February 2013) (Learn how and when to remove this message) |
Edmund M. Clarke | |
|---|---|
 | |
| Born | Edmund Melson Clarke, Jr. (1945-07-27)July 27, 1945 Newport News, Virginia, U.S. |
| Died | December 22, 2020(2020-12-22) (aged 75) |
| Education | University of Virginia (BA) Duke University (MA) Cornell University (PhD) |
| Known for | Model checking |
| Awards | A.M. Turing Award |
| Scientific career | |
| Fields | Computer science |
| Institutions | Carnegie Mellon University |
| Thesis | Completeness and Incompleteness Theorems for Hoare-Like Axiom Systems (1976) |
| Doctoral advisor | Robert Lee Constable |
| Doctoral students | |
| Website | www |
Edmund Melson Clarke, Jr. (July 27, 1945 – December 22, 2020) was an Americancomputer scientist andacademic noted for developingmodel checking, a method forformally verifyinghardware andsoftware designs. He was theFORE Systems Professor ofComputer Science atCarnegie Mellon University. Clarke, along withE. Allen Emerson andJoseph Sifakis, received the 2007ACMTuring Award.
Born inNewport News, Virginia, Clarke received aB.A. degree inmathematics from theUniversity of Virginia,Charlottesville, in 1967, anM.A. degree inmathematics fromDuke University,Durham NC, in 1968, and aPh.D. degree incomputer science fromCornell University,Ithaca, New York, in 1976. After receiving his Ph.D., he taught in the Department of Computer Science atDuke University, for two years. In 1978, he moved toHarvard University,Cambridge, Massachusetts, where he was an assistant professor of computer science in theDivision of Applied Sciences. He left Harvard in 1982 to join the faculty in the Computer Science Department atCarnegie Mellon University,Pittsburgh, Pennsylvania. He was appointed full professor in 1989. In 1995, he became the first recipient of theFORE Systems Professorship, an endowed chair in theCarnegie Mellon School of Computer Science. He became a university professor in 2008 and became an emeritus professor in 2015.[2]
He died fromCOVID-19 in December 2020, at age 75, during theCOVID-19 pandemic in Pennsylvania.[3][4]
Clarke's interests includedsoftware andhardwareverification andautomatic theorem proving. In his Ph.D. thesis he proved that certainprogramming language control structures did not have goodHoare-style proof systems. In 1981 he and his Ph.D. studentE. Allen Emerson first proposed the use ofmodel checking as a verification technique forfinite-state concurrent systems. His research group pioneered the use ofmodel checking forhardware verification. Symbolicmodel checking usingbinary decision diagrams was also developed by his group. This important technique was the subject ofKenneth L. McMillan's Ph.D. thesis, which received anACM DoctoralDissertation Award. In addition, his research group developed the first parallelresolutiontheorem prover (Parthenon) and a theorem prover based on a symbolic computation system (Analytica).[5] In 2009, he led the creation of the Computational Modeling and Analysis of Complex Systems (CMACS) center, funded by theNational Science Foundation. This center has a team of researchers, spanning multiple universities, applyingabstract interpretation andmodel checking to biological andembedded systems.
Clarke was afellow of theACM and theIEEE. He received a Technical Excellence Award from theSemiconductor Research Corporation in 1995 and anAllen Newell Award for Excellence in Research from theCarnegie MellonComputer Science Department in 1999. He was a co-winner along withRandal Bryant, Emerson, and McMillan of theACMParis Kanellakis Award in 1999 for the development ofsymbolic model checking. In 2004 he received theIEEE Computer SocietyHarry H. Goode Memorial Award for significant and pioneering contributions to formal verification of hardware and software systems, and for the profound impact these contributions have had on the electronics industry. He was elected to theNational Academy of Engineering in 2005 for contributions to the formal verification of hardware and software correctness. He was elected to theAmerican Academy of Arts and Sciences in 2011. He received theHerbrand Award in 2008 in "recognition of his role in the invention of model checking and his sustained leadership in the area for more than two decades." In 2012, hereceived an honorary doctorate fromTU Wien for his outstanding contributions to the field of informatics. He received the 2014Bower Award and Prize for Achievement in Science from theFranklin Institute for "his leading role in the conception and development of techniques for automatically verifying the correctness of a broad array of computer systems, including those found in transportation, communications, and medicine." He was a member ofSigma Xi andPhi Beta Kappa.
