EE5122 PA2 Part 2: CPAchecker Algorithm Comparison on SV-COMP ReachSafety
收藏DataCite Commons2026-05-03 更新2026-05-07 收录
下载链接：
https://zenodo.org/doi/10.5281/zenodo.19547601
下载链接
链接失效反馈官方服务：
资源简介：
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.
提供机构：
Zenodo
创建时间：
2026-04-13
