Reproduction Package for ASE 2023 Submission `Improving Verification through Compiler Optimizations'

Artifact

In order to run this artifact please clone sv-benchmarks into this folder. Afterwards you can just run the program using the running instructions down below. The results used in the paper can be found in the folder transformation-for-verification-data.

Setup

In order to setup this project, first initialize the submodules or clone this repository with the flag --recursive. Afterwards execute python3 src/setup.py in this directory, in order to add the required files to the submodules.

Running

In order to run this locally inside ./src

./main_bench.py --specification specification/path.prp program/to/verify.c

For example:

./main_bench.py --specification ../setup-files/test-run/unreach-call.prp ../setup-files/test-run/test_program.c

In order to execute with benchexec, execute the following insider ./src, after adapting bench.xml to suit your purposes:

./benchmark_local.sh