Model checking is a formal verification technique for determining whether a system model satisfies specified logical properties. It is used to analyze correctness, safety, and reliability in systems where exhaustive or systematic state exploration is possible.
In computer science, model checking or property checking is, for a given model of a system, exhaustively and automatically checking whether this model meets a given specification. Typically, one has hardware or software systems in mind, whereas the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems.