The basic form for running the analyses in the ISSTA 2006 paper is:
jpf -c <relevant configuration> <ContainerClass> parameters

The parameters are in the form:
<sequence-length> [<# of parameters>] <search-type>

The number of parameters is optional since the symbolic 
analysis don't require this. The search-type can be one of the
following:

Concrete cases:

	  0 - Random
	  1 - Classic Model Checking
	  6 - Shape Abstraction Matcing
	  7 - Full Container State Matching

Symbolic cases:

	  0 - Random
	  1 - Classic Model Checking
	  6 - Symbolic Execeution with Shape Abstraction
	  7 - Symbolic Execeution with Subsumption Checking

For Random one must load the rand.properties file and 
for Classic Model Chekcing one needs the mc.properties file and
for option 6 and 7 one needs the test.properties configuration.

For random the number of paths considered can be set in the 
rand.properties file.

Some examples are:

jpf -c rand.properties issta2006.TreeMap.EnvTreeMap 15 5 0

This will run TreeMap concretely with sequence length 15 and 
5 parameters in Random search mode

jpf -c mc.properties issta2006.TreeMap.EnvTreeMap 15 5 1

Will do the same thing but in Classic model checking mode.

jpf -c test.properties issta2006.TreeMap.EnvTreeMap 15 5 6

Now using shape abstractions.

jpf -c test.properties issta2006.TreeMap.EnvTreeMap 15 5 7

And now using the full container matching.

jpf -c symbolic.properties issta2006.TreeMap.EnvSymTreeMap 8 7

Will run the symbolic version of TreeMap for sequence length 8
using symbolic subsumption checking.

NOTE: The provided libararies for the decision procedures are only compiled for Linux and hence for now
Symbolic Execution only works under Linux and requires the LD_LIBRARY_PATH variable to be set to
<jpf-home>/extensions/symbolic/csrc

For running BinomialHeap one will just change the class to:

issta2006.BinomialHeap.EnvBinomialHeap for concrete and
issta2006.BinomialHeap.EnvSymBinomialHeap for symbolic.

Lastly, the files are set up for predicate coverage and the
JPF_* files need to be changed by commenting out a few lines 
for checking basic block coverage - the location of these are
documented in the files.