Java PathFinder (JPF) is a popular model checker for Java
programs. JPF was used to generate object graphs as test inputs for
object-oriented programs. Specifically, JPF was used as an
implementation engine for the Korat algorithm. Korat takes two
inputs--a Java predicate that encodes properties of desired object
graphs and a bound on the size of the graph--and generates all graphs
(within the given bound) that satisfy the encoded properties. Korat
uses a systematic search to explore the bounded state space of object
graphs. Korat search was originally implemented in JPF using a simple
instrumentation of the Java predicate. However, JPF is a
general-purpose model checker and such direct implementation results
in an unnecessarily slow search. We present our results on speeding up
Korat search in JPF. The experiments on ten data structure subjects
show that our modifications of JPF reduce the search time by over an
order of magnitude.