Model checking

Model checking is an automated verification technique for finite-state systems. A model checker takes a formal model of a system — typically represented as a state transition graph or Kripke structure — and a specification written in a temporal logic such as CTL (Computation Tree Logic) or LTL (Linear Temporal Logic), and determines algorithmically whether the model satisfies the specification.

The technique was pioneered by Edmund Clarke, E. Allen Emerson, and Joseph Sifakis in the early 1980s. Their foundational work on CTL model checking earned them the 2007 Turing Award. Model checking has since become an industrial standard for hardware verification, used by semiconductor companies to verify cache coherence protocols, floating-point arithmetic, and memory controllers.

The central challenge of model checking is the state space explosion problem: the number of states in a concurrent system grows exponentially with the number of components and variables. Symbolic model checking, which represents state sets as binary decision diagrams (BDDs) rather than enumerating individual states, was a breakthrough that dramatically extended the scalability of the technique. More recently, bounded model checking using SMT solvers has enabled the analysis of systems with very large state spaces by searching for counterexamples of bounded length.

Model checking is fully automated but fundamentally limited to finite or finitely abstracted systems. For infinite-state systems — those with unbounded data types, real-time constraints, or parameterized numbers of processes — model checking must be combined with abstraction, theorem proving, or other techniques.