Dr. Edmund Melson Clarke, Jr.

Clarke's interests include software and hardware verification and automatic theorem proving. 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 his 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).