NTUEE FM PA2 Part2 — CPAchecker ReachSafety reproduction artifact

Fuente: Zenodo
Saved in:
Bibliographic Details
Main Author: Sun, Shuo-Heng
Format: Recurso digital
Published: Zenodo 2026
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866902068864745472
author Sun, Shuo-Heng
author_facet Sun, Shuo-Heng
contents <p>This record archives the <span class="font-semibold">PA2 Part 2</span> reproduction package for a CPAchecker + BenchExec study on <span class="font-semibold">SV-COMP ReachSafety</span> tasks. It bundles <span class="font-semibold">four</span> configurations (<span class="font-semibold">value analysis</span>, <span class="font-semibold">predicate abstraction</span>, <span class="font-semibold">BMC</span>, <span class="font-semibold">k-induction</span>) over <span class="font-semibold">five</span> base categories (<span class="font-semibold">BitVectors</span>, <span class="font-semibold">ControlFlow</span>, <span class="font-semibold">ECA</span>, <span class="font-semibold">Loops</span>, <span class="font-semibold">Sequentialized</span>), with limits <span class="font-semibold">300 s wall / 15 GB RAM / 2 CPU cores</span> per run (see <code class="md-clickable-code md-inline-path-filename-like"><span class="md-inline-path-prefix">bench-defs/</span><span class="md-inline-path-filename">cpa_alg_eval_part2.xml</span></code>). The ZIP includes <span class="font-semibold"><code class="">cpachecker/</code></span>, <span class="font-semibold"><code class="">bench-exec-src/</code></span>, <span class="font-semibold"><code class="">sv-benchmarks/</code></span>, <span class="font-semibold"><code class="">bench-defs/</code></span>, and <span class="font-semibold"><code class="md-inline-path-filename-like"><span class="md-inline-path-prefix">results/part2/</span></code></span> (BenchExec <code class="">*.xml.bz2</code> plus merged HTML/CSV tables). <span class="font-semibold">Step-by-step reproduction</span> is in <span class="font-semibold"><code class="md-clickable-code md-inline-path-filename-like"><span class="md-inline-path-filename">README.md</span></code></span> at the root of the extracted folder.</p>
format Recurso digital
id zenodo_https___doi_org_10_5281_zenodo_20193184
institution Zenodo
language
publishDate 2026
publisher Zenodo
record_format zenodo
spellingShingle NTUEE FM PA2 Part2 — CPAchecker ReachSafety reproduction artifact
Sun, Shuo-Heng
<p>This record archives the <span class="font-semibold">PA2 Part 2</span> reproduction package for a CPAchecker + BenchExec study on <span class="font-semibold">SV-COMP ReachSafety</span> tasks. It bundles <span class="font-semibold">four</span> configurations (<span class="font-semibold">value analysis</span>, <span class="font-semibold">predicate abstraction</span>, <span class="font-semibold">BMC</span>, <span class="font-semibold">k-induction</span>) over <span class="font-semibold">five</span> base categories (<span class="font-semibold">BitVectors</span>, <span class="font-semibold">ControlFlow</span>, <span class="font-semibold">ECA</span>, <span class="font-semibold">Loops</span>, <span class="font-semibold">Sequentialized</span>), with limits <span class="font-semibold">300 s wall / 15 GB RAM / 2 CPU cores</span> per run (see <code class="md-clickable-code md-inline-path-filename-like"><span class="md-inline-path-prefix">bench-defs/</span><span class="md-inline-path-filename">cpa_alg_eval_part2.xml</span></code>). The ZIP includes <span class="font-semibold"><code class="">cpachecker/</code></span>, <span class="font-semibold"><code class="">bench-exec-src/</code></span>, <span class="font-semibold"><code class="">sv-benchmarks/</code></span>, <span class="font-semibold"><code class="">bench-defs/</code></span>, and <span class="font-semibold"><code class="md-inline-path-filename-like"><span class="md-inline-path-prefix">results/part2/</span></code></span> (BenchExec <code class="">*.xml.bz2</code> plus merged HTML/CSV tables). <span class="font-semibold">Step-by-step reproduction</span> is in <span class="font-semibold"><code class="md-clickable-code md-inline-path-filename-like"><span class="md-inline-path-filename">README.md</span></code></span> at the root of the extracted folder.</p>
title NTUEE FM PA2 Part2 — CPAchecker ReachSafety reproduction artifact
url https://doi.org/10.5281/zenodo.20193184