Experiments

1. Experimental Setup

For reference, our experiments are performed on a 2.80 GHz Intel(R) Core(TM) i7-7600 machine with 8 GB memory, running 64-bit Windows 10. The timeout per benchmark is set to 3600sec (1h); the memory limit to 4 GB.

2. Reproduce Experiments

The benchmarks used in our paper can be found in the directoryexamples/cav19_bm. Various batch scripts have been included for reproducing the experiments.

Remark:

• For benchmark 01/German-1 and 02/German-2, our script only reproduces the experiments with invariants.


• Per suggestion from the instruction of artifact submission, we exclude from the artifact two time-consuming benchmarks 04/TokenRing-fixed and 07/openWSN.


• We did not collect memory usage as doing this in Windows batch script is painful. We manually collected the information of memory usage reported in the paper.

Step 1. Compile benchmarks

To compile benchmarks, please execute the following command:

compile-benchmark.bat

To clean up benchmarks, please execute the following command:

cleanup-benchmark.bat

Step 2. Run experiments

To reproduce the experiments, please execute the following command:

run-experiments.bat

The experiments will generate logs. Read the README.txt to get more on how to read the log files.

Step 3. Process results

Warning: To use the process-results scripts, please make sure you have Python (version 2.7.14 or above) installed on your machine.

To process the experimental results, e.g. executing time etc., please execute the following command:

process-results.bat

After running the above script, the results will be stored in the following two files:

• pat_ptester.csv: the results of running PAT and PTester atop which our tool is built; the comparison demonstrates the overhead our approach adds it on.
• pati.csv: the experimental result of PAT+I; only 01/German-1 and 02/German-2 have such results.