Edmund Melson Clarke

Leader in the development of model checking. Discovered that even complex hardware and software designs can be viewed as very large finite-state systems. Contributions to the development of model checking include the original formulation, application to hardware verification, Binary-Decision Diagram-based symbolic model checking that exploits system modularity by partitioning the transition relation, SAT-based bounded model checking, and state space reduction by automated abstraction. Model-checking tools are widely used by computer manufacturers such as Intel, IBM, Fujitsu, Sun, and SGI. Editor in chief, Formal Methods in System Design. Co-founder, the international conference on Computer-Aided Verification (CAV). Co-recipient, Association for Computing Machinery (ACM) Turing Award, considered the Nobel Prize of computer science. First recipient, FORE Systems Professorship. Fellow, ACM, Institute of Electrical and Electronic Engineers, and National Academy of Engineering.