Edmund Melson Clarke, Jr.
-
(b.) -1945 July 27(d.)2020 December 22
Bio/Description
Clarke's interests included 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 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).
-
Date of Birth:
1945 July 27 -
Date of Death:
2020 December 22 -
Gender:
Male -
Noted For:
Developer for model checking, a method for formally verifying hardware and software designs -
Category of Achievement:
-
More Info: