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>