Edmund M. Clarke

A grouping.

Two bodies of work by one person: where proof-based verification stops -- completeness and incompleteness for Hoare-like axiom systems, the language constructs for which no good axiomatisation exists, and the characterisation problem -- and then the state-space alternative he built instead, from synchronisation skeletons through automatic verification of finite-state concurrent systems to symbolic model checking. The records arrived under four spellings, now joined, and the split ran almost exactly between the two lines, so a reader following either would not have found the other.