tacas-reproducibility

TACAS Reproducibility

Use this before submission (for tool papers, before the mandatory artifact deadline) and again

before camera-ready. At TACAS reproducibility is not a courtesy: for a regular tool or

tool-demonstration paper the artifact is mandatory and feeds acceptance, and for a research

or case-study paper a voluntary artifact earns the title-page badges. The goal is that an ETAPS

evaluator, on a clean virtual machine, can rebuild your evidence and reach your numbers.

Design for the clean ETAPS VM

The artifact process assumes a provided VM image with bounded evaluator time. Package accordingly:

[Self-contained]  ship a VM-ready package: a Dockerfile or a pinned environment (lockfile), with
                  the tool prebuilt; not "apt-get install 30 things and hope"
[Offline]         no network access at run time; vendor every dependency, benchmark, and model
[Bounded]         a short smoke run that finishes in minutes, plus a documented full run with its
                  expected (possibly long) runtime
[Deterministic]   fix seeds and tool options; state what is and is not deterministic
[Documented]      a README that orients an evaluator in one screen: what it is, how to run the
                  smoke test, how to reproduce each claim, expected outputs and runtimes

Claim-to-script mapping (the heart of a TACAS artifact)

• Map each reported table, figure, and headline number to a script and its expected output.
• Provide a top-level reproduce/ (or equivalent) that regenerates results from logged data,

and a separate path that re-runs the tool from scratch for those who have the time budget.

• State the machine you produced the numbers on; evaluators on different hardware should still see

the same verdicts and the same relative comparison even if wall-clock differs.

Claim-to-evidence audit

| Claim in the paper | Weak artifact answer | TACAS-ready answer |

|---|---|---|

| "Solves N benchmarks" | "Benchmarks available on request" | The exact task set vendored + a script printing solved/unsolved |

| "Faster than <baseline>" | Only your tool shipped | Both tools (or the baseline's install) with the equal-budget harness |

| "Sound / sound up to k" | Verdicts unchecked | A validation script (witness checking / cross-tool agreement) |

| "The counterexample is real" | Prose only | A replayable witness the evaluator can validate |

"Available on request" and "works on our cluster" are treated as not reproducible at TACAS;

convert every such line into a concrete, VM-runnable script.

Degrees of reproducibility (state the one you achieved)

• Turnkey: one documented command regenerates each table/figure from logged data on the VM.
• Scripted: scripts exist but need documented manual steps or a large external benchmark

download.

• Descriptive: prose detailed enough that a competent reader could rebuild the pipeline.

For a tool paper, aim turnkey for the smoke run and the headline comparison — that is what the

AEC checks against the Functional (and ideally Reusable) badge. Large full-benchmark runs

may stay scripted with the time budget documented. Stating the achieved level honestly beats

promising turnkey behaviour that fails on the clean VM.

Category difference

• Regular tool / tool-demonstration: the artifact is mandatory, submitted right after the

paper, evaluated with the PC — plan it as a co-equal deliverable, not a follow-up.

• Regular research / case-study: the artifact is voluntary and post-acceptance; if you want

the badges, prepare it after notification, but the paper must already be self-contained on the

evidence side.

Consistency and camera-ready pass

• Before submission (or the artifact deadline): every scored number traces to a VM-runnable script;

the paper and artifact agree; for a research paper the artifact is anonymized (no owner

strings, cluster paths, lab names, identity-revealing repo URLs).

• Before camera-ready: swap any anonymized/placeholder location for a permanent, DOI-issuing archive

(Zenodo/figshare/Software Heritage) and align with the badges you earned (tacas-artifact-evaluation).

Output format

[Claim inventory] <claim -> script -> expected output>
[Clean-VM readiness] runs offline on a fresh VM? smoke test in minutes? yes/no
[Reproducibility level] turnkey / scripted / descriptive, stated honestly
[Soundness/validation] <witness or cross-tool check present? yes/no>
[Category obligation] mandatory (tool/tool-demo) / voluntary (research/case-study)
[Fixes before upload] <ordered list>