Edmund Melson Clarke, Jr. (July 27, 1945 – December 22, 2020) was an American computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs.
[5] In 2009, he led the creation of the Computational Modeling and Analysis of Complex Systems (CMACS) center, funded by the National Science Foundation.
This center has a team of researchers, spanning multiple universities, applying abstract interpretation and model checking to biological and embedded systems.
He was a co-winner along with Randal Bryant, E. Allen Emerson, and Kenneth McMillan of the ACM Paris Kanellakis Award in 1999 for the development of symbolic model checking.
He received the Herbrand 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."
He received the 2014 Bower Award and Prize for Achievement in Science from the Franklin 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."