Property-Specific Heuristics: They are based on specific properties such as:
Deadlock: Maximize number of blocked threads
Assertions and exceptions: Minimize distance to assertions and throws of explicit exceptions
Language-specific size constraints such as overflow of a particular buffer
Resource consumption: e.g., attempts to exceed the limit on open file handles
A lot of the work on model checking using heuristics largely concentrates on property-based heuristics. Selecting such heuristics in practice is not easy, particularly when the model checker is applied to a large concurrent program with many types of errors (e.g., assertions, potential for deadlocks, uncaught exceptions). Also, it is not always possible to know during model checking how close you are to a property violation.