cav-artifact-evaluation

CAV Artifact Evaluation

Use this for the artifact track. CAV artifact evaluation is run by a dedicated **Artifact Evaluation

Committee (AEC), is invited but optional after notification, and — importantly — final paper

acceptance is not conditional on it. Authors declare artifact intent at submission time**; the

actual AEC submission comes after acceptance, on the artifact track's own deadline (CAV 2026 artifact

registration: 22 Apr 2026). Two things to internalize: badges are earned by AEC members actually

running your package, and for anonymized paper categories the review-time material and the AEC

artifact are handled differently (the AEC artifact is post-notification, so de-anonymization is fine).

The three badges (verify the current set and names)

| Badge | What it certifies | What earns it |

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

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

| Functional | The artifact is documented, consistent, complete, and exercisable | A clean-machine install, a working run, and documented expected outputs |

| Reusable | Quality significantly exceeds Functional; others can build on it | Functional plus a reuse license, clear structure, and easy-to-adapt docs; requires Available |

Available is a low-cost, high-value badge (archive the package with a DOI). Functional and Reusable

require the AEC's own run to succeed, so the failure mode is almost always "it did not build/run on

their machine," not "the idea was weak." Reusable additionally requires that the artifact already be

Available.

How the AEC evaluates (two phases, ≥2 reviewers)

Each artifact is examined by at least two AEC members across two phases:

[Smoke-test phase]  reviewers confirm the artifact downloads, unpacks, and the basic entry point
                    runs on a clean environment. Fix any friction here and you can still respond.
[Full-review phase] reviewers work through the claims: run the tool on the benchmarks, check the
                    documented outputs, and assess reusability for the Reusable badge.

Design so the smoke test succeeds in the first ten minutes on a fresh machine — a VM image or a

container removes most smoke-test failures.

What AEC reviewers open first (verification-specific)

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

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

| A solver / model checker / prover | Build/install + one benchmark run | Undocumented dependencies; only-builds-on-authors'-machine |

| A benchmark comparison | The scripts that reproduce the paper's table | Numbers in the PDF no script regenerates; unpinned benchmark set |

| A soundness claim | The witness/certificate + an independent checker | "Verified" verdict with no checkable proof |

| A randomized/portfolio tool | Seeds, resource limits, and core counts | Non-deterministic results with no fixed seed or stated limits |

Packaging plan for a verification artifact

[Container]    ship a Docker image or a VM (many CAV artifacts use a provided VM) with the tool
               pre-built; avoid "compile these dependencies by hand"
[README]       one-screen orientation: what it is, install, a smoke-test command, how to reproduce
               each table, expected runtime and outputs, and the hardware you used
[Benchmarks]   the exact benchmark set and revision (SV-COMP/SMT-COMP/HWMCC/VNN-COMP subset), or a
               documented fetch; state the subset and why
[Config]       resource limits (time/memory), core count, seeds for any randomized component
[Witnesses]    proof certificates / unsat proofs / verification witnesses + an independent checker
               where the claim is correctness
[Mapping]      an explicit table: paper claim -> script/command -> expected result
[License]      an OSI-approved license so the artifact can be badged Reusable
[Archive]      deposit in a DOI-issuing repository for the Available badge

Worked vignette: packaging an SMT-solver + benchmark study

A Regular Paper contributes a solving technique and a benchmark comparison. To target Reusable and

Available: ship a Docker image with the solver pre-built; a smoke.sh that solves one bundled

instance in under a minute; a reproduce/ directory whose scripts rerun the benchmark division under

the paper's exact time/memory limits and regenerate each table; the pinned benchmark-set revision (or

a fetch script); logged seeds for the portfolio; DRAT/unsat proofs with a bundled checker for the

UNSAT claims; a claim-to-command mapping in the README; and an Apache/MIT license. State honestly

which results are turnkey and which need the full (multi-day) benchmark run, and archive the whole

package on Zenodo for a DOI.

Calibration

• Artifact evaluation is after notification and not a condition of acceptance — plan it, but

do not block the camera-ready on the badge outcome.

• Badge names, the exact set offered, the phase structure, and whether the AEC is single- or

double-anonymous vary by cycle — confirm on the current Artifact Evaluation page.

Output format

[Target badges] Available / Functional / Reusable
[Phase readiness] smoke test passes in <10 min on a clean machine? yes/no
[Contents] <tool/benchmarks(revision)/config(limits,seeds)/witnesses/license>
[Claim mapping] <claim -> command -> expected result present? yes/no>
[Archive] DOI-issuing repository chosen? yes/no
[Fixes before submission] <ordered list>