Structural Heuristics: Structural coverage measures can be used during directed model checking to improve the state space coverage (Groce and Visser 2002). Rather than looking for a particular error, it may be best to try and explore the structure of the program systematically, looking for any kind of error. As noted before, this is the motivation behind coverage metrics in testing. For example, you can guide the model checker to pick parts of the state space to analyze based on structural coverage of the code that would generate those state spaces. A simple example would be to consider only statement coverage: If the model checker can next analyze a program statement that has never executed, versus one that has, then it picks the new one. This simple example is a greedy algorithm which may not work. We will describe some of the structural heuristics that have been found to be useful for model checking.