- Given a finite-state model of a system, exhaustively check the evolved state space for certain properties
- Not a formal proof
- When properties do not hold, the checker tries to report counter examples
- Safety Properties: “Something bad will never happen”
- Liveness Properties: “Something will eventually happen”
- Associated with Temporal Logic, a type of Modal Logic