A lot of information about JPF can be found here.

More information can be found here.

To configure JPF, you may want to use a jpf.properties file containing

search.class = gov.nasa.jpf.search.heuristic.HeuristicSearch
search.heuristic.class = 
  gov.nasa.jpf.search.heuristic.BFSHeuristic

to use a breadth-first traversal of the state space (rather than a depth-first traversal which is the default). To check for race conditions, you may want to add

jpf.listener = gov.nasa.jpf.tools.precise.PreciseRaceDetector

to your jpf.properties file.

To check some properties of our solution to the readers-writers problem by means of JPF, we modified our solution as follows.