If you encounter any problems with the instructions below, please contact Thomas Lemberger for support.
Replication Package & Virtual Machine
We provide a replication package for reproducing our experimental results.
The easiest way to use it is with our virtual machine.
We assume that your machine meets the following or similar requirements:
- Operating system based on Linux 4.x
- OpenJDK 1.8 (or compatible)
- 16 GiB of RAM
- At least 2 CPU cores
We also assume that you use bash as your command-line shell.
In the following, we will refer to the directory test-study of the extracted replication package as $BASE.
We use BenchExec for our experiments, which allows isolated, reproducible execution of benchmarks. It is already installed on the virtual machine provided. If you don't have BenchExec installed, our replication package contains a debian package for easy installation. From $BASE, run the following on the command line:
After installation, you will have to add your user to group benchexec manually:
sudo gpasswd -a $USER benchexec
For more information and support, see the benchexec documentation.
To execute our experiments with TBF, use the benchmark definition iuv_benchmark_ex.xml (iuv was the working name of TBF). It contains one run definition per test tool (+ klee-replay). To execute all run definitions, run from the directory of the extracted replication package:
PYTHONPATH=./lib/ benchexec iuv_benchmark_ex.xml
All results will be in $BASE/tbf/results.
To execute our experiments with the model checkers,
- For CBMC:
benchexec --container cbmc.xml
The results for cbmc will be in $BASE/cbmc/results
- For CPA-Seq:
benchexec --container cpa-seq.xml
The results for CPA-Seq will be in $BASE/cpa-seq/results
- For the two configurations of ESBMC:
benchexec --container esbmc-incr.xml
benchexec --container esbmc-kind.xml
The results for ESBMC-incr and ESBMC-kInd will be in $BASE/esbmc/results
- For CBMC:
To visualize the created results, you can use the tool table-generator, which is part of BenchExec.
We provide a table definition to create one big table with all results:
table-generator -x teststudy_all.xml
This will only work if the directory structure is according to the steps specified above.
table-generator will produce one HTML and one CSV-file. To open the HTML, run
To validate the witnesses produced by the model checkers, run:
To validate witnesses with CPAchecker:
benchexec --container cpa-seq-validate-cbmc.xml
benchexec --container cpa-seq-validate-cpa-seq.xml
benchexec --container cpa-seq-validate-esbmc-incr.xml
benchexec --container cpa-seq-validate-esbmc-kind.xml
To validate witnesses with CPA-witness2test:
benchexec --container cpa-w2t-validate-cbmc.xml
benchexec --container cpa-w2t-validate-cpa-seq.xml
benchexec --container cpa-w2t-validate-esbmc-incr.xml
benchexec --container cpa-w2t-validate-esbmc-kind.xml
To validate witnesses with FShell-witness2test:
benchexec --container fshell-w2t-validate-cbmc.xml
benchexec --container fshell-w2t-validate-cpa-seq.xml
benchexec --container fshell-w2t-validate-esbmc-incr.xml
benchexec --container fshell-w2t-validate-esbmc-kind.xml
To validate witnesses with Ultimate Automizer:
benchexec --container uautomizer-validate-cbmc.xml
benchexec --container uautomizer-validate-cpa-seq.xml
benchexec --container uautomizer-validate-esbmc-incr.xml
benchexec --container uautomizer-validate-esbmc-kind.xml
You will find the results of the validation runs in the corresponding results directories.
After executing all these steps, you should have produced the data provided above yourself. Feel free to play around with the tools some more. If you have any questions regarding our work, the virtual machine or the results, you can write us at email@example.com. And if you are curious about our other publications, visit sosy-lab.org.