2007 · Languages & software
Model checking turns a system’s behaviour into a graph that can be explored automatically.
Visual guide
Describe states and transitions.
Write the required property.
Find a proof or a counterexample.
Automated verification became a practical tool for finding subtle defects in hardware and software.
The state space can become enormous, and checking a model does not automatically validate the model’s faithfulness.
01 · The idea
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.
Automated verification became a practical tool for finding subtle defects in hardware and software.
02 · The people
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.
Read the biography ↗
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.
Read the biography ↗
Joseph Sifakis independently pioneered model checking, developing methods for verifying the behavior of finite-state systems. His work in France connected formal models with tools for analyzing systems that interact continuously with their environments. He helped establish the Verimag laboratory and later studied rigorous design for embedded systems. His contribution to the joint award lies in both verification theory and the practical construction of dependable reactive systems.
Read the biography ↗03 · Read further
Original explanations based on the official award record. The subject label is an editorial navigation aid.
Automata, grammars and algorithms helped make compilers teachable and dependable.
The story
Abstraction lets a system change inside while preserving its promises outside.
The story