Model-driven verification, as implemented in the SPIN tool, advocates the use of abstraction mappings during concrete model checking to efficiently analyze an under-approximation of the feasible behaviors of a system. All reported counterexamples correspond to real errors. The model checker traverses the concrete transitions of the analyzed system and for each explored concrete state it stores an abstract version of that state. The abstract state, computed by an abstraction mapping provided by the user, is used to determine whether the model checker’s search should continue or backtrack (if the abstract state has been visited before). This allows for detection of subtle errors which cannot be discovered with classic techniques.