EE5122 PA2 Part 2: CPAchecker Algorithm Comparison on SV-COMP ReachSafety

Reproduction artifact for EE5122 Formal Methods PA2 Part 2. Contains BenchExec results for 4 CPAchecker algorithms (predicate abstraction, value analysis, BMC, k-induction) on 5 SV-COMP ReachSafety categories (BitVectors, ControlFlow, Loops, ECA, Sequentialized). 10,328 total verification runs with 300s/2GB resource limits. What's new in v2.1 Bundled CPAchecker binary (~500 MB) - the precompiled tool from upstream artifact 10.5281/zenodo.11070973. Bundled sv-benchmarks subset (~54 MB) - 4 of 5 ReachSafety categories. ReachSafety-ECA (~1.9 GB) is omitted; mount the upstream tree to reproduce ECA. LICENSE file (Apache 2.0 + MIT mix, inherited from upstream). Dockerfile for turnkey reproduction (Ubuntu 24.04 + OpenJDK 17 + BenchExec 3.33). Related identifiers: cites the FSE 2024 paper (10.1145/3660797) and isDerivedFrom the upstream artifact (10.5281/zenodo.11070973). Version history v1 (2026-04-13): initial deposit - XMLs, scripts, results only. v2 (2026-04-30): added pre-computed summary tables and per-algorithm CSV. v2.1 (2026-05-03): added CPAchecker bundle, sv-benchmarks subset, LICENSE, Dockerfile, related_identifiers.