JPF is, in essence, a Java virtual machine (itself written in Java) and this enables JPF to control and measure many aspects of software's execution.
it can enumerate and control the choices made at non-deterministic points in the program, such as the generation of pseudo-random numbers and most importantly for the experiments here the interleaving of separate threads in concurrent program.