tacas-artifact-evaluation

TACAS Artifact Evaluation

Use this for the artifact track. TACAS treats the artifact as a first-class citizen, and the

process differs from most venues in two ways: for tool papers it is **mandatory and runs in

parallel with paper review, and badging follows the ETAPS Artifact Badge** guidelines, decided

by the Artifact Evaluation Committee (AEC) and printed on the paper's title page.

The two rounds (know which one you are in)

| Round | Applies to | Timing | Consequence |

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

| Round 1 — mandatory | Regular tool + tool-demonstration papers | Submitted right after the paper, evaluated with the PC | Outcome feeds the acceptance decision |

| Round 2 — voluntary | Regular research + case-study papers | After acceptance notification | Earns title-page badges; does not gate acceptance |

The consequence for a tool paper is blunt: a package that does not build or run on the clean

evaluation VM can cost the paper, not merely a badge. Treat the artifact as a co-equal deliverable

due about two weeks after the paper.

The ETAPS Artifact Badges

| Badge | What it certifies | What earns it |

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

| Available | The artifact is permanently, publicly retrievable | Deposit in a DOI-issuing archive (Zenodo, figshare, Software Heritage) |

| Functional | The artifact runs and does what the paper says | A clean-VM install, a smoke run, and documented expected outputs |

| Reusable | Others can build on and adapt it | The Functional bar plus careful docs, structure, licensing, and generality |

The AEC decides which subset a given artifact receives. Available is low-cost, high-value (archive

the package); Functional and Reusable require the evaluator's own run to succeed on the provided

VM, so the failure mode is always "did not run in their environment," never "the idea was weak."

What the AEC opens first

| Claim type | First thing inspected | Common failure caught |

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

| A verification tool | The README and one smoke command on the VM | Undocumented deps; needs network; only-builds-on-authors'-machine |

| A benchmark comparison | The script that regenerates the headline table | Numbers in the PDF no script reproduces |

| A soundness claim | The validation / witness-checking path | "Fast" results that were never checked for correctness |

| A tool-demonstration | The documented demo walkthrough | The demo the paper describes cannot be driven on the VM |

Assume a bounded evaluator time budget on the clean ETAPS VM. Design for the first ten minutes

to succeed: a smoke run that finishes fast and prints an expected output.

Packaging plan

[VM-ready]    a package that builds/runs inside the provided VM image, offline, deps vendored
[README]      one screen: what it is, smoke run, per-claim reproduction, expected outputs + runtimes
[Mapping]     an explicit table: paper claim -> script -> expected result
[Benchmarks]  the actual task set vendored (or documented access), not just a pointer
[Validation]  a witness-checking or cross-tool script for any soundness/correctness claim
[License]     an OSI-approved license so the artifact can be badged Reusable
[Archive]     deposit in a DOI-issuing repository for the Available badge (esp. at camera-ready)

Anonymity by category (do not get this backwards)

• Round-1 tool / tool-demo artifacts are single-blind — they may carry the tool identity and

authorship, matching the single-blind paper.

• Round-2 research artifacts are submitted after acceptance, so anonymity is no longer the

concern; but a research review artifact attached to the double-blind paper (if you choose to

supply one at submission) must be anonymized — no owner strings, lab names, or identity-revealing

repository URLs.

Worked vignette: badging a model-checking tool

A regular tool paper contributes a new checker. To target Available + Functional + Reusable: ship a

VM-ready image with the tool prebuilt; a smoke.sh that verifies one small bundled task in under a

minute; a reproduce/ directory whose scripts regenerate the benchmark table from logged runs; a

claim-to-script mapping in the README; the vendored benchmark set; a witness-validation script for

the soundness claim; and an Apache/MIT license. State honestly which results are turnkey and which

need the full (slow) benchmark run. Deposit the final version on Zenodo for the DOI.

Calibration

• The badge set, the round structure, and the VM image are set per edition on the tacas.info

artifact page — confirm the current guidelines and image before packaging.

• Do not conflate the mandatory Round-1 deadline with the voluntary Round-2 or the camera-ready;

they are distinct dates.

Output format

[Round] mandatory (tool/tool-demo, PC-parallel) / voluntary (research/case-study, post-acceptance)
[Target badges] Available / Functional / Reusable
[Clean-VM test] does build + smoke run succeed offline on the provided VM? yes/no
[Claim mapping] <claim -> script -> expected result present? yes/no>
[Archive] DOI-issuing deposit ready for Available? yes/no
[Fixes before upload] <ordered list>