Edmund Melson Clarke, Jr.

Developer of model checking, Clarke pioneered a method for formally verifying hardware and software designs. In his Ph.D. thesis he proved that certain programming language control structures did not have good Hoare style proof systems. In 1981 he and his Ph.D. student E. Allen Emerson first proposed the use of Model checking as a verification technique for finite state concurrent systems.

His research group pioneered the use of Model checking for hardware verification. Symbolic Model checking using BDDs was also developed by Clarke's group. This important technique was the subject of Kenneth McMillan's Ph.D. thesis, which received an ACM Doctoral Dissertation Award.

In addition, his research group developed the first parallel resolution theorem prover (Parthenon) and the first theorem prover to be based on a symbolic computation system (Analytica).