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 , 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>
Source: brycewang-stanford/Awesome-Journal-Skills → CAV-Skills/skills/cav-reproducibility/SKILL.md
1---2name: cav-reproducibility3description: Use when strengthening CAV (Computer Aided Verification) reproducibility, covering benchmark provenance (SV-COMP/SMT-COMP/HWMCC/VNN-COMP set revisions), pinned tool and baseline versions, resource limits and hardware, seeds for randomized/portfolio solvers, checkable proof witnesses/certificates for soundness claims, and consistency between the paper's tables and the artifact.4---567# CAV Reproducibility89Use this before submission and again before camera-ready. In computer-aided verification,10reproducibility is not a courtesy — a benchmark result is only meaningful relative to a **fixed11benchmark set, pinned tool versions, and a stated resource budget**, and a soundness claim is only12credible if it ships a **checkable witness**. The goal is that a competent reader could rerun your13evaluation and re-check your correctness claims and reach your conclusions.1415## Evidence map1617- Map each theorem, technique claim, and reported benchmark number to a **verifiable location** — a18 proof (body or appendix), a script in the artifact, or a table regenerated from logged runs.19- For techniques, give enough of the algorithm, parameters, and encoding that a reader could20 re-implement or rerun it.21- For benchmark evaluations, report the exact **benchmark set and revision**, the **baseline tools22 and versions**, the **resource limits** (per-instance time and memory), the **hardware and core23 count**, and the **number of runs**.24- For soundness claims, emit a **certificate/witness** (unsat proof, DRAT, an SV-COMP-style25 witness, an Isabelle/Coq script) and an independent checker — a bare "verified" verdict is not26 reproducible evidence.27- Keep the paper and the artifact **consistent**: a number in the PDF that no script regenerates is28 the contradiction reviewers read as carelessness.2930## The reproducibility failure modes CAV reviewers know3132| Claim in the paper | Weak answer | CAV-ready answer |33|---|---|---|34| "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 |35| "Solves N hard instances" | "on standard benchmarks" | The named division of set <revision R>, the exact instance list, the fetch/pin in the artifact |36| "Our result is sound/UNSAT" | asserted | The unsat proof + a bundled independent checker that accepts it |37| "Randomized search finds it" | one lucky run | Fixed seed(s), number of runs, variance reported |38| "Scales to large designs" | "large" | The size metric and the largest instance run, with the timeout that bounds it |3940## Provenance and configuration pinning4142```text43[Benchmarks] pin the set + revision (SV-COMP/SMT-COMP/HWMCC/VNN-COMP subset); archive the instance44 list and the fetch script, not just "the standard benchmarks"45[Tools] record exact versions (yours and every baseline), build flags, and the commit/tag46[Limits] state per-instance wall-clock and memory limits, core count, and the hardware/CPU47[Randomness] log seeds for portfolio/stochastic components; say what is and is not deterministic48[Witnesses] ship proof certificates + an independent checker for every soundness/UNSAT claim49[Runs] state the number of repetitions and how variance/timeouts were handled50```5152## Degrees of reproducibility (state the one you achieved)5354- **Turnkey:** one documented command reruns a benchmark subset and regenerates a table/figure from55 logged data (and re-checks the witnesses).56- **Scripted:** scripts exist but require documented manual steps, a large external benchmark57 download, or a long (multi-day) full run.58- **Descriptive:** prose detailed enough that a competent reader could rebuild the evaluation.5960For CAV, aim turnkey for anything a reviewer might rerun quickly (a solver on a small bundled subset,61a witness check) and scripted-with-clear-instructions for a full multi-day benchmark sweep. Stating62the achieved level honestly beats promising turnkey behavior that fails on a clean machine.6364## Vignette: a portfolio-solver evaluation6566Consider a paper claiming a portfolio SMT technique is faster and stays sound. Its reproducibility67spine: the solver pinned to a commit with build flags; each baseline pinned to a released version and68its documented configuration; the benchmark division pinned to a revision with an archived instance69list; a uniform per-instance time/memory limit and stated hardware; logged seeds and repetition70count; a differential check against a trusted solver on all verdicts (no disagreements) plus unsat71proofs with a bundled checker; and analysis scripts that turn the logs into the paper's tables — with72one honest sentence about the parts (a proprietary hardware benchmark, say) that cannot be shared and73why.7475## Consistency and camera-ready pass7677- Before submission: every benchmark number traces to a logged run in the artifact; every soundness78 claim has a checkable witness; the artifact is anonymized for Regular/Application categories.79- Before camera-ready: swap anonymized links for a permanent, DOI-issuing archive, and align the80 artifact with the AEC badges you are pursuing (`cav-artifact-evaluation`).8182## Output format8384```text85[Claim inventory] <claim -> proof/witness or logged benchmark run>86[Benchmark provenance] set+revision / baseline versions / limits / hardware — pinned? yes/no87[Soundness evidence] witness + independent checker present? yes/no88[Reproducibility level] turnkey / scripted / descriptive, stated honestly89[Paper fixes] <must appear in the PDF>90[Artifact fixes] <additions before upload>91```9293---9495**Source:** [`brycewang-stanford/Awesome-Journal-Skills`](https://github.com/brycewang-stanford/Awesome-Journal-Skills) → `CAV-Skills/skills/cav-reproducibility/SKILL.md`
thedixitjain