Model Checking
Model checking exhaustively verifies whether all states of a system satisfy temporal-logic properties, automatically finding counterexample states that violate them.
Purpose
Exhaustively verify safety and liveness of concurrent systems, automatically discovering deadlocks and races.
Mechanism
Models the system as a state machine and expresses properties in temporal logic (LTL/CTL). Explicit state enumeration or symbolic BDDs traverse all states. If a property fails, a counterexample path is produced. SPIN and NuSMV are common tools.
Use cases
- Concurrency verification
- Protocol verification
- Hardware verification