Model Checking

Model checking is a technique in formal verification that automatically determines whether a finite-state model of a system satisfies a property expressed in temporal logic, and if not, produces a concrete counterexample trace. Unlike theorem proving, model checking requires no human guidance once the model and property are specified: it is fully automatic. The technique has found real security flaws in protocols that survived years of expert review — most famously, the Needham-Schroeder protocol flaw discovered by Gavin Lowe in 1995 using seventeen lines of specification and a model checker. The core limitation is the state space explosion problem: the number of states grows exponentially with the number of concurrent processes, making model checking tractable for hardware and protocols but challenging for general software. Symbolic model checking (using Binary Decision Diagrams) and SAT-based bounded model checking have extended the tractable frontier substantially. Model checking cannot verify systems with unbounded state, placing it in a well-defined region below the ceiling imposed by Rice's theorem. For any property richer than finite-trace reachability, the undecidability barrier is encountered.