A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
Model checking is an automated verification technique that exhaustively explores every reachable state of a finite-state system to determine whether a given specification holds. The system is modeled as a state-transition graph, the specification is expressed in temporal logic, and the model checker systematically visits all reachable states. If a violation is found, the tool produces a counterexample — a concrete execution trace demonstrating the failure. Model checking is fully automatic (no invariants or proofs required) but faces the state explosion problem: the number of states grows exponentially with the number of system components.
Model checking takes a fundamentally different approach from deductive verification (Hoare logic, weakest preconditions). Instead of constructing proofs, it exhaustively searches the state space of a system. You build a formal model of the system as a finite-state machine (or a composition of such machines for concurrent systems), express the desired property in temporal logic ("every request is eventually granted," "the system never enters a deadlock state"), and let the tool check every reachable state. If the property holds in all states, the system is verified. If not, the tool returns a counterexample: a specific sequence of states demonstrating the violation.
The appeal of model checking is full automation — no loop invariants, no proof strategies, no human guidance beyond the model and the specification. The model checker is a "push-button" tool: provide the inputs and wait for the answer. This makes it accessible to engineers who are not verification experts. The counterexamples it produces are concrete and actionable, showing exactly which sequence of events leads to the failure. For concurrent systems, where race conditions depend on specific thread interleavings that are nearly impossible to reproduce by testing, this exhaustive exploration is uniquely valuable.
The central challenge is the state explosion problem. A system of n concurrent processes, each with k states, has up to kn reachable states. For realistic systems, this number is astronomical. A protocol with 10 processes each having 100 states has 1020 states — more than any computer can enumerate one by one. Three major families of techniques address this. Symbolic model checking (using BDDs or SAT solvers) represents sets of states implicitly using Boolean formulas rather than enumerating them individually, handling billions of states. Abstraction (notably CEGAR) reduces the model to a smaller abstract version, verifying the abstract model and refining it only when spurious counterexamples arise. Partial-order reduction exploits the observation that many interleavings of independent actions lead to the same result, pruning redundant exploration.
Model checking has been spectacularly successful in hardware verification (Intel uses it extensively to verify processor designs after the Pentium FDIV bug) and protocol verification (finding bugs in cache coherence protocols, network protocols, and security protocols). For software, the technique is more limited because software systems are often infinite-state (unbounded data, recursion, dynamic allocation), requiring abstraction to finite models. Tools like SPIN (for protocol models in Promela), NuSMV (for hardware in SMV), and CBMC (bounded model checking for C code) represent different points in the design space. The 2007 Turing Award to Clarke, Emerson, and Sifakis recognized model checking as one of the most impactful contributions to software and hardware reliability.