01 · A life in computing
The person behind the work
E. Allen Emerson co-developed model checking with Edmund Clarke, showing how temporal-logic properties of finite-state systems could be checked automatically. His work emphasized the logical foundations of verification and the relationship between a system’s possible executions and the properties users want guaranteed. At the University of Texas at Austin, he continued research on formal methods. He shared the award with Clarke and Joseph Sifakis.
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.