Backward and parallel exploration techniques for Java PathFinder

Model checking software programs is an effective approach for finding bugs in program by systematically exploring the entire program's state space. One big issue with model checker is state space explosion. Recent research techniques like Partial Order Reduction and symmetry reductions help in reducing the state explosion but it is still infeasible to model check real world programs. JPF is one such explicit-state model checker designed for Java programs and provides non-deterministic choices and thread scheduling control. JPF uses state backtracking and state comparison to eliminate states that are already executed in the past but still cannot cope with state explosion. We tackle this problem in a different way i.e. by enabling concurrent execution of the state space by different workers. The key insight here is to be able to explore the state space from an arbitrary point and be able to go in any direction i.e. backwards or forwards. We present a new search strategy to explore state space. Using this, we can arbitrarily divide the search space into multiple workers without having to worry about expensive state comparisons or transmitting them on network. However this may result in non-equal division of work between the workers because of the inherent underlying search tree. We further build on this work to develop a near optimal work partitioning strategy by employing Work Sharing and Work Stealing approaches instead of static state partitioning using hash sets. Our techniques help in automated test generation and general state exploration for bug finding. We introduce a novel approach to divide the search space, for concurrent execution, without incurring network communication overhead and build on that to provide a more work optimal solution. We evaluated the technique on standard single and multi-threaded Java programs to show the efficacy of our approach.