## Artifact for Submission 172:

### Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers

- Checklist
- Tool
- Documentation
- Tutorial
- 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 directory`examples/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.