Part 1

So far I have been reading the papers that have been published regarding Java Path Finder. In the paper "Model Checking Programs" by Visser et al. they describe the symmetry reductions that are done in the Java Path Finder code stating that they are closely related to the Partial Order Reduction rules that are described in the Holzmann and Peled paper from 1994.

I have also been reading the Slides "Model Checking Programs with Java Path Finder". It describes two different ways that they are using POR. On the one hand they are using it regarding scheduling relevance, which is the normal domain of POR. This is determining when a thread interleaving matters. On the other hand they are using it to detect race conditions on shared objects.