Reproduction Artifact: Evaluating CPAchecker Verification Algorithms on Five ReachSafety Categories (FM PA2, Spring 2026)

Reproduction Artifact: Evaluating CPAchecker Verification Algorithms on Five ReachSafety Categories Abstract This artifact reproduces an evaluation that compares four verification algorithms implemented in **CPAchecker 3.0** on five `ReachSafety` base categories of the **SV-COMP** benchmark suite. The algorithms are: Value Analysis (`--valueAnalysis`) -- explicit tracking of variable values Predicate Abstraction (`--predicateAnalysis`) -- CEGAR-based predicate abstraction with interpolation BMC (`--bmc-incremental`) -- incremental Bounded Model Checking k-Induction (`--kInduction`) -- k-induction-based verification Tasks were proportionally sampled (~27%) from each category to keep the experiment feasible on a single workstation. After BenchExec filtered tasks against the `unreach-call` property, **408 benchmarks** remained, giving **1632 tool runs** (4 algorithms x 408 benchmarks). The complete set of raw `.xml.bz2` result files, BenchExec log archives, HTML / CSV tables generated by `table-generator`, the benchmark XML, the sampled `.set` files, and the scripts that produced them are all included. Observations The three observations below are stated per ReachSafety base category and are supported by the per-category breakdown in [tables/comparison.html](tables/comparison.html) (full table) and [tables/comparison-diff.html](tables/comparison-diff.html) (tasks where algorithms disagree). The exact counts come from `tables/comparison.csv` and can be regenerated with `python3 scripts/analyze_results.py`. Observation 1 -- ReachSafety-Loops: BMC finds the most bugs On the **212** Loops tasks that passed property filtering, **BMC produced 37 correct alarms** (`false(unreach-call)`), more than **k-induction (33)**, **value analysis (23)** and **predicate abstraction (20)**. BMC also returned the largest total of correct verdicts on this category (**109**, vs. 104 for k-induction, 71 for predicate abstraction and 32 for value analysis). This matches the SV-COMP-style intuition that bounded model checking is the strongest bug hunter when bug depth fits the unrolling bound. Observation 2 -- ReachSafety-Recursive: only BMC and k-induction can analyze any task Out of **42** Recursive tasks, both **value analysis** and **predicate abstraction** scored **0 correct** and reported `ERROR (recursion)` on **41** tasks each (one further timed out). With the chosen options (no recursion support enabled), they cannot complete a single recursive program in our sample. **BMC** and **k-induction** each solved **1** task and produced the same `ERROR (recursion)` on **41** tasks. The Recursive category therefore acts as a *kill test* for the two non-recursion-aware configurations. Observation 3 -- ReachSafety-Arrays: predicate abstraction is repeatedly defeated by interpolation failures Out of **123** Arrays tasks, **predicate abstraction** produced **32** `ERROR (interpolation failed)` results (about **26%** of the category) on top of 66 timeouts, ending with only **22** correct verdicts. **BMC** (26 correct) and **k-induction** (24 correct) avoided this error class entirely (0 interpolation errors), at the cost of more out-of-memory results (10 OOM each, vs. 3 for predicate abstraction). Interpolation-based abstraction is therefore the weakest of the three non-value configurations on array-heavy programs in our setup. Contents ``` FM-PA2-Part2-artifact/ README.md # this file cpa_alg_eval.xml # BenchExec benchmark definition (4 algs x 5 categories) sets/ # proportionally sampled .set files Arrays-sample.set BitVectors-sample.set ControlFlow-sample.set Loops-sample.set Recursive-sample.set results/ # raw experimental data (BenchExec output) cpa_alg_eval.<timestamp>.results.value-analysis.xml.bz2 cpa_alg_eval.<timestamp>.results.predicate-abstraction.xml.bz2 cpa_alg_eval.<timestamp>.results.BMC.xml.bz2 cpa_alg_eval.<timestamp>.results.k-induction.xml.bz2 cpa_alg_eval.<timestamp>.results.txt # BenchExec text summary cpa_alg_eval.<timestamp>.logfiles.zip # per-task CPAchecker logs tables/ # HTML + CSV comparison tables comparison.html # main side-by-side table (rendered in a browser) comparison-diff.html # tasks where algorithms disagree comparison.csv # raw data scripts/ sample_sets.py # regenerates sets/*-sample.set gen-table.sh # runs table-generator on merged result files analyze_results.py # prints per-category, per-algorithm statistics package-artifact.sh # rebuilds the zip and prints the SHA256 ``` Requirements Hardware used in the reference run CPU: AMD Ryzen 7 9700X (8 cores / 16 threads) RAM: 32 GB physical (~29 GiB usable) Storage: about 2 GB free for results and logs Software - **Ubuntu 22.04 LTS or later** (the reference run used Ubuntu 26.04 LTS, kernel 7.0.0). The SoSy-Lab VM ([10.5281/zenodo.8245829](https://doi.org/10.5281/zenodo.8245829)) is an acceptable alternative. - **OpenJDK 17** (`sudo apt install openjdk-17-jdk-headless`) - **BenchExec 3.34 or newer** (provides both `benchexec` and `table-generator`) - **lxcfs** (`sudo apt install lxcfs && sudo systemctl enable --now lxcfs`) -- silences the host-metadata-leak warning - **CPAchecker 3.0** -- the unmodified release zip is sufficient - **SV-COMP benchmark set** -- the [sv-benchmarks](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks) Git repository. The reference run used commit `aee7887414c1e89fb6dba1e1a6ecd13b688063e7` (2026-05-05). The artifact itself is fully self-contained for **inspection** and **analysis re-runs**: opening `tables/comparison.html` in a browser, parsing `tables/comparison.csv`, and running `python3 scripts/analyze_results.py` require **no additional downloads** beyond a system Python 3. To **re-run the BenchExec experiment from scratch**, CPAchecker and the sv-benchmarks repository must be obtained separately (see Step 2 below).