Model Checking

An automatic verification technique that exhaustively explores the state space of a formal model of a system (usually a finite‑state transition system) to determine whether the model satisfies a specification expressed in a temporal or modal logic, producing counterexample traces when the property is violated.

Model checking is the algorithmic verification process that explores a formal model's state space to determine whether it satisfies a given specification, often expressed in temporal or modal logics.