Ranged Model Checking

D. Funes, J. H. Siddiqui, and S. Khurshid
ACM SIGSOFT Software Engineering Notes 37(6) and The Java Pathfinder Workshop (JPF 2012)


We introduce ranged model checking, a novel technique for more effective checking of Java programs using the Java PathFinder (JPF) model checker. Our key insight is that the order in which JPF makes non-deterministic choices de- fines a total ordering of execution paths it explores in the program it checks. Thus, two in-order paths define a range for restricting the model checking run by defining a start point and an end point for JPF’s exploration. Moreover, a given set of paths can be linearly ordered to define con- secutive, (essentially) non-overlapping ranges that partition the exploration space and can be explored separately. While restricting the run of a model checker is a well-known tech- nique in model checking, the key novelty of our work is con- ceptually to restrict the run using vertical boundaries rather than the traditional approach of using a horizontal bound- ary, i.e., the search depth bound. Initial results using our prototype implementation using the JPF libraries demon- strate the promise ranged model checking holds.
(JPF 2012), Cary, NC, November 2012, Page 1-5


@inproceedings { jpf2012,
author = { }, }