01 · A life in computing
The person behind the work
Edmund Clarke helped turn formal verification into automated model checking. With E. Allen Emerson he showed how to check temporal properties of finite-state systems, and later work addressed the enormous state spaces found in practical hardware and software. At Carnegie Mellon he helped develop methods and tools that made verification more scalable. His contribution connected mathematical specification with automated searches for errors and evidence of correctness.
The contribution, explained
Edmund Clarke, E. Allen Emerson and Joseph Sifakis developed model checking. A finite model describes a system’s states and transitions; a logical property describes what should hold. An algorithm explores the model and can return a counterexample showing how a requirement fails.
Why it matters
Automated verification became a practical tool for finding subtle defects in hardware and software.