Thread Preference Heuristic: This is similar to the thread interleaving heuristic mentioned above except that it focuses on a few threads that may be suspected to harbor an error. To do this, it relies on the knowledge of what parts of the system are “interesting.” For example, when JPF was applied to the Remote Agent example, the race detection algorithm was used in a first run of the model checker with the BFS search strategy to identify a number of potential race conditions. Allowing the race detection to run for 3 minutes revealed that the Executive and Planner threads had unprotected write accesses to a field. The threads involved in the potential race conditions were then used to guide a thread-preference search with a similarly small queue, and a counterexample was quickly detected. This approach scaled to larger versions of the Remote Agent than other heuristics could handle. This is a different flavor of structural heuristic than those presented previously. It relies on specific knowledge of the program’s behavior that can be observed by the model checker (which branches are taken, which threads are enabled, etc.) during the execution of the program. In certain cases, such as the one described above, this knowledge can be automatically extracted by the model checker itself. Such additional knowledge can, as expected, aid a guided search considerably.