Model checking Java programs using structural heuristics
Alex Groce, Willem I. Visser · ACM SIGSOFT Software Engineering Notes · 2002
We describe work in troducing heuristic search into the Java PathFinder model checker, which targets Java bytecode. Rather than focusing on heuristics aimed at a particular kind of error (such as deadlocks) we describe heuristics based on a modification of traditional branch coverage metrics and other structure measures, such as thread inter-dependency. We present experimental results showing the utility of these heuristics, and argue for the usefulness of structural heuristics as a class.