Uloženo v:
| Hlavní autor: | |
|---|---|
| Médium: | Recurso digital |
| Jazyk: | |
| Vydáno: |
Zenodo
2026
|
| On-line přístup: | https://doi.org/10.5281/zenodo.20002104 |
| Tagy: |
Přidat tag
Žádné tagy, Buďte první, kdo vytvoří štítek k tomuto záznamu!
|
| _version_ | 1866902086220775424 |
|---|---|
| author | Wu, YD |
| author_facet | Wu, YD |
| 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> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_20002104 |
| institution | Zenodo |
| language | |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | EE5122 PA2 Part 2: CPAchecker Algorithm Comparison on SV-COMP ReachSafety Wu, YD <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> |
| title | EE5122 PA2 Part 2: CPAchecker Algorithm Comparison on SV-COMP ReachSafety |
| url | https://doi.org/10.5281/zenodo.20002104 |