Supplementary Materials for
Compositional Partial Order Reduction for Concurrent Systems

This is a supplementary page for the experiment in Compositional Partial Order Reduction for Concurrent Systems. This page is maintained by Tian Huat Tan, and he can be reached by , any questions regarding the experiments is welcome.

1. Instruction

In this section, instructions of downloading the PAT tool and how to verify an Orc Model with PAT is given.

1. Please download the PAT tool here.
2. After opening PAT, select File > Open and open the Orc Model file.
3. After loading the Orc Model file, click Verification (F7) for verification.
4. Select a property of interest in the list box, checked Partial Order Reduction to perform verfication WITH Compositional Partial Order Reduction; if it is unchecked, verification will be performed WITHOUT partial order reduction.
5. Click Verify to perform verfication, and the result of verification will be shown in the output window.

2. Models Used

Following table provides the Orc models used in the experiment.

Alternatively, you can also download all models in zip format here.