THE MODEL CHECKER explore every reachable state, and hand back the trace that breaks the rule
Testing samples a few runs; model checking explores them all. Cast a system as a finite state machine, state a safety property (“the two trains are never on the bridge at once”), and mechanically search the entire reachable state space. If the bad state is reachable, the checker does not just say “unsafe” — it returns the exact counterexample trace, the sequence of steps that leads to disaster. Exhaustive falsification, with a receipt.
THE TECHNIQUE search all reachable states; a reachable bad state = a counterexample trace
Compute the reachable set of a small transition system by fixpoint, then test the safety property “the bad state is never reached.” With edges leading to it, the checker finds the violation: live demo
HISTORY & CREDIT Clarke–Emerson & Queille–Sifakis, 1981
“You can only test a few paths, so bugs always hide in the ones you missed.” — not for a finite-state system: a model checker visits every reachable state. If a violation exists, it will be found — and reported as a concrete trace you can replay. Coverage becomes total, not sampled. cited
1981 · Clarke & Emerson (USA) and Queille & Sifakis (France) — independently invent temporal-logic model checking: verify a property over all states. 2007 · Turing Award — to Clarke, Emerson & Sifakis for model checking. now · SPIN, TLA+, and hardware verification catch concurrency bugs no test suite could sample.
The counterexample trace is the model checker's gift: not “a bug exists somewhere” but “do exactly this and it breaks.” Exhaustive search turns the impossible testing question into a finite, answerable one. 1981
RECOMMEND FOR I-13 reachability of a bad state, exhaustively, computed
On the canonical compiler, reachability is computed by fixpoint over the transition relation; with the edge into the bad state present, the safety property is violated:
$ i13 run modelcheck.i13 # edges 0->1->2->3, bad state = 3
bad_reachable = 1 -- state 3 IS reachable (trace 0->1->2->3): safety VIOLATED
Recommend: the model checker is LIT for I-13 — verified by fixpoint that the bad state 3 is reachable from the start via 0→1→2→3 (safety violated); remove the edge and it becomes unreachable (safe). It falsifies over the entire reachable state space at once — and returns the trace, not just a verdict.