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.

/**
 * This class represents a database.  There are many competing
 * threads wishing to read and write.  It is acceptable to have
 * multiple processes reading at the same time, but if one thread
 * is writing then no other process may either read or write.
 */
public class Database
{
  private int readers; // number of active readers
  private int writers; // number of active writers
 
  /**
     Initializes this database.
  */
  public Database()
  {
    this.readers = 0;
  }
 
  /**
     Read from this database.
 
     @param number Number of the reader.
  */
  public void read(int number)
  {
    synchronized(this)
    {
      this.readers++;
      System.out.println("Reader " + number + " starts reading.");
    }
 
    final int DELAY = 5000;
    try
    {
       Thread.sleep((int) (Math.random() * DELAY));
    }
    catch (InterruptedException e) {}
 
    assert((this.writers == 1 && this.readers == 0) || this.writers == 0);
 
    synchronized(this)
    {
      System.out.println("Reader " + number + " stops reading.");
      this.readers--;
      if (this.readers == 0)
      {
        this.notifyAll();
      }
    }
  }
 
  /**
     Writes to this database.
 
     @param number Number of the writer.
  */
  public synchronized void write(int number)
  {
    while (this.readers != 0)
    {
      try
      {
        this.wait();
      }
      catch (InterruptedException e) {}
    }
    System.out.println("Writer " + number + " starts writing.");
    this.writers++;
 
    final int DELAY = 5000;
    try
    {
      Thread.sleep((int) (Math.random() * DELAY));
    }
    catch (InterruptedException e) {}
 
    assert((this.writers == 1 && this.readers == 0) || this.writers == 0);
 
    this.writers--;
    System.out.println("Writer " + number + " stops writing.");
    this.notifyAll();
  }
}