Cav reproducibility

CAV Reproducibility

Use this before submission and again before camera-ready. In computer-aided verification, reproducibility is not a courtesy — a benchmark result is only meaningful relative to a fixed benchmark set, pinned tool versions, and a stated resource budget, and a soundness claim is only credible if it ships a checkable witness. The goal is that a competent reader could rerun your evaluation and re-check your correctness claims and reach your conclusions.

Evidence map

• Map each theorem, technique claim, and reported benchmark number to a verifiable location — a proof (body or appendix), a script in the artifact, or a table regenerated from logged runs.
• For techniques, give enough of the algorithm, parameters, and encoding that a reader could re-implement or rerun it.
• For benchmark evaluations, report the exact benchmark set and revision, the baseline tools and versions, the resource limits (per-instance time and memory), the hardware and core count, and the number of runs.
• For soundness claims, emit a certificate/witness (unsat proof, DRAT, an SV-COMP-style witness, an Isabelle/Coq script) and an independent checker — a bare "verified" verdict is not reproducible evidence.
• Keep the paper and the artifact consistent: a number in the PDF that no script regenerates is the contradiction reviewers read as carelessness.

The reproducibility failure modes CAV reviewers know

Claim in the paper	Weak answer	CAV-ready answer
"Faster than solver X"	"X was slower in our tests"	X vA.B, its documented config, same time/memory limit, same hardware; per-instance data in the artifact
"Solves N hard instances"	"on standard benchmarks"	The named division of set <revision R>, the exact instance list, the fetch/pin in the artifact
"Our result is sound/UNSAT"	asserted	The unsat proof + a bundled independent checker that accepts it
"Randomized search finds it"	one lucky run	Fixed seed(s), number of runs, variance reported
"Scales to large designs"	"large"	The size metric and the largest instance run, with the timeout that bounds it

Provenance and configuration pinning

[Benchmarks] pin the set + revision (SV-COMP/SMT-COMP/HWMCC/VNN-COMP subset); archive the instance
             list and the fetch script, not just "the standard benchmarks"
[Tools]      record exact versions (yours and every baseline), build flags, and the commit/tag
[Limits]     state per-instance wall-clock and memory limits, core count, and the hardware/CPU
[Randomness] log seeds for portfolio/stochastic components; say what is and is not deterministic
[Witnesses]  ship proof certificates + an independent checker for every soundness/UNSAT claim
[Runs]       state the number of repetitions and how variance/timeouts were handled

Degrees of reproducibility (state the one you achieved)

• Turnkey: one documented command reruns a benchmark subset and regenerates a table/figure from logged data (and re-checks the witnesses).
• Scripted: scripts exist but require documented manual steps, a large external benchmark download, or a long (multi-day) full run.
• Descriptive: prose detailed enough that a competent reader could rebuild the evaluation.

For CAV, aim turnkey for anything a reviewer might rerun quickly (a solver on a small bundled subset, a witness check) and scripted-with-clear-instructions for a full multi-day benchmark sweep. Stating the achieved level honestly beats promising turnkey behavior that fails on a clean machine.

Vignette: a portfolio-solver evaluation

Consider a paper claiming a portfolio SMT technique is faster and stays sound. Its reproducibility spine: the solver pinned to a commit with build flags; each baseline pinned to a released version and its documented configuration; the benchmark division pinned to a revision with an archived instance list; a uniform per-instance time/memory limit and stated hardware; logged seeds and repetition count; a differential check against a trusted solver on all verdicts (no disagreements) plus unsat proofs with a bundled checker; and analysis scripts that turn the logs into the paper's tables — with one honest sentence about the parts (a proprietary hardware benchmark, say) that cannot be shared and why.

Consistency and camera-ready pass

• Before submission: every benchmark number traces to a logged run in the artifact; every soundness claim has a checkable witness; the artifact is anonymized for Regular/Application categories.
• Before camera-ready: swap anonymized links for a permanent, DOI-issuing archive, and align the artifact with the AEC badges you are pursuing (cav-artifact-evaluation).

Output format

[Claim inventory] <claim -> proof/witness or logged benchmark run>
[Benchmark provenance] set+revision / baseline versions / limits / hardware — pinned? yes/no
[Soundness evidence] witness + independent checker present? yes/no
[Reproducibility level] turnkey / scripted / descriptive, stated honestly
[Paper fixes] <must appear in the PDF>
[Artifact fixes] <additions before upload>