• 1945 July 27
    (b.) - ?


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).
  • Date of Birth:

    1945 July 27
  • Gender:

  • Noted For:

    Developer for model checking, a method for formally verifying hardware and software designs
  • Category of Achievement:

  • More Info: