A model checker is used in code verification. They take some form of finite (but very large) state space model and verify properties. The simplest method is to try every single state value and/or path exhaustively, but for larger state spaces some form of abstract representation is used to make the problem tractable.
Used in Chap. 6: page 89