Reproduction Package — FM PA2 Part 2

Formal Methods — Artifact Preparation This reproduction package accompanies the FM PA2 Part 2 assignment (CPAchecker + BenchExec on ReachSafety benchmarks).It bundles CPAchecker 4.2.2 (Unix binary layout under cpachecker/), SV-COMP task definitions under sv-benchmarks/, BenchExec benchmark XML in bench-defs/, a Makefile for runs and tables, raw BenchExec outputs under results-part2/, and this README. The layout is intentionally similar to the Part 1 artifact template (DarIsmcTransferability-artifact-FSE24-proceedings): bundled tool + benchmarks + bench-defs + Makefile + precomputed results/-style data. Contents Item Role README.md This file Makefile Check environment, run BenchExec, generate HTML tables bench-defs/part2-reachsafety-four-techs.xml Tasks, resource hints, four CPAchecker configurations cpachecker/ CPAchecker installation root (bin/cpachecker) sv-benchmarks/ SV-COMP benchmarks (needs c/properties/unreach-call.prp and the .set files referenced in the XML) results-part2/ Raw .xml.bz2, .results.txt, logfiles.zip, and .table.html from our run Requirements Linux with BenchExec 3.x (e.g. pip install --user benchexec; then python3 -m benchexec.check_cgroups). If cgroups fail, use make check-soft only for a sanity check — execution may still work depending on your setup. Java compatible with CPAchecker 4.x (see CPAchecker). For a turnkey environment similar to published artifacts, the SoSy-Lab Ubuntu VM is suitable; install BenchExec inside the VM if it is missing. Populate sv-benchmarks/ from the official SV-COMP repository (sv-benchmarks on GitLab) or copy sv-benchmarks/ from DarIsmcTransferability-artifact-FSE24-proceedings in this course workspace so versions stay aligned with Part 1. Experimental settings Tool: CPAchecker 4.2.2, property unreach-call (sv-benchmarks/c/properties/unreach-call.prp). Configurations (four run definitions): value analysis (--valueAnalysis), predicate abstraction (--predicateAnalysis), bounded model checking (--bmc-incremental), k-induction (--kInduction). Common options: --no-output-files --heap 13000M --option cpa.predicate.memoryAllocationsAlwaysSucceed=true (plus propertyfile from BenchExec — do not duplicate --spec). Resource limits: 300 s soft / 360 s hard CPU time, 15 GB RAM, 1 CPU core per task (outer limits in Makefile: BX_TIME, BX_MEM; meets the assignment minimum of 300 s and 2 GB). Parallelism: default 8 jobs (BENCHEXEC_JOBS=-N 8); reduce if memory is tight. Five ReachSafety base categories (see XML): ReachSafety-ControlFlow, ReachSafety-BitVectors, ReachSafety-Recursive, ReachSafety-VerifyThis-Loops, ReachSafety-VerifyThis-Recursive. Full detail is in bench-defs/part2-reachsafety-four-techs.xml. TL;DR — reproduce From the root of this package (directory that contains Makefile, bench-defs/, cpachecker/, sv-benchmarks/): make check # or: make check-soft make run-part2 # long run; log: results-part2/benchexec-run.log make table # merged HTML for all tasks (uses newest stamp or TABLE_STAMP=...) make tables-per-category Optional: make run-part2-tmux for a detached session; make tail-run-log to follow the log. Pin a run when generating tables (example stamp from our machine): make table TABLE_STAMP=2026-05-06_00-33-09 make tables-per-category TABLE_STAMP=2026-05-06_00-33-09 Note: make table must use only the four aggregate files *.results.{value,predabs,bmc,kind}.xml.bz2 for one stamp — do not mix per-category splits into the same table-generator invocation (empty table symptom). Obtaining CPAchecker Download the official CPAchecker 4.2.2 Unix archive from cpachecker.sosy-lab.org, unzip, and place the distribution so that ./cpachecker/bin/cpachecker exists. Alternatively copy cpachecker/ from the Part 1 artifact (older CPAchecker versions may require adjusting the benchmark XML for CLI compatibility). Three observations (evaluation) Statistics below use BenchExec category correct on run stamp 2026-05-06_00-33-09, validated on ControlFlow + BitVectors (122 tasks: 73 + 49). Evidence: per-category HTML under results-part2/results.2026-05-06_00-33-09.ReachSafety-{ControlFlow,BitVectors}.table.html, quantile views in the merged table (regenerate with make table TABLE_STAMP=2026-05-06_00-33-09). More correct verdicts with predicate abstraction and k-induction. On ControlFlow ∪ BitVectors, predicate abstraction and k-induction yield substantially more correct results than value analysis and BMC: Configuration Correct (CF + BV) value 41 predabs 76 bmc 44 kind 67 Runtime on correct runs (≤ 20 s CPU). Counting only correct tasks with cputime ≤ 20 s: predabs (68) > kind (58) > value (39) ≈ bmc (36). Open the HTML table’s Quantile view for CPU time — the ordering is consistent with these counts. Recursive and VerifyThis sets are poorly handled under these default configurations: Recursive is dominated by errors; VerifyThis-Loops and VerifyThis-Recursive exhibit almost no robust correct outcomes across all four engines. Use them to discuss limitations, not as the main fairness comparison between techniques.