Saved in:
| Main Author: | |
|---|---|
| Format: | Recurso digital |
| Language: | |
| Published: |
Zenodo
2026
|
| Online Access: | https://doi.org/10.5281/zenodo.20002104 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Table of Contents:
- <p>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.</p><h3>What's new in v2.1</h3><ul><li>Bundled CPAchecker binary (~500 MB) - the precompiled tool from upstream artifact 10.5281/zenodo.11070973.</li><li>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.</li><li>LICENSE file (Apache 2.0 + MIT mix, inherited from upstream).</li><li>Dockerfile for turnkey reproduction (Ubuntu 24.04 + OpenJDK 17 + BenchExec 3.33).</li><li>Related identifiers: cites the FSE 2024 paper (10.1145/3660797) and isDerivedFrom the upstream artifact (10.5281/zenodo.11070973).</li></ul><h3>Version history</h3><ul><li>v1 (2026-04-13): initial deposit - XMLs, scripts, results only.</li><li>v2 (2026-04-30): added pre-computed summary tables and per-algorithm CSV.</li><li>v2.1 (2026-05-03): added CPAchecker bundle, sv-benchmarks subset, LICENSE, Dockerfile, related_identifiers.</li></ul>