cav-experiments

name	cav-experiments
description	Use when designing or auditing a CAV (Computer Aided Verification) empirical evaluation, covering standard benchmark sets (SV-COMP/SMT-COMP/HWMCC/VNN-COMP), fair baseline solvers with pinned versions and equal resource limits, timeout-dominated comparisons, soundness cross-checks and proof witnesses, cactus/scatter reporting, and matching evidence to the shape of each verification claim.

CAV Experiments

Use this before submission when the evaluation is not yet locked. CAV reviewers are verification researchers; the empirical section is where a good technique is won or lost. The organizing principle is evidence proportional to the claim — the evaluation must test what the paper asserts, on benchmarks and baselines a skeptic accepts, under a resource budget that makes the comparison fair.

Evaluation audit

• Match evidence to the claim shape. A soundness claim needs a proof and/or a checkable witness, not a benchmark score. A performance claim needs a fair comparison on standard benchmarks under equal limits. A capability claim ("solves instances prior tools cannot") needs those instances and the prior tools actually run.
• Use standard benchmark sets at a pinned revision (SV-COMP, SMT-COMP, HWMCC, VNN-COMP, or a documented domain set). State the subset you ran and why; a hand-picked set invites the "cherry-picked" reject.
• Choose fair baselines: the strongest relevant prior tool(s), at their latest released version, run with a documented, equal resource limit (per-instance time and memory) on the same hardware. An outdated or mis-configured baseline is a scored weakness.
• Respect that verification comparisons are timeout-dominated. Report the limit explicitly; distinguish solved / unsolved / timeout / memout / error; and prefer cactus plots (instances solved vs. time) and scatter plots (per-instance head-to-head) over a single mean that a few timeouts distort.
• Cross-check soundness. Run a differential check against a trusted tool on all verdicts and report disagreements (ideally none); ship proof witnesses where correctness is the claim.
• Design limits in, not on: know before you run which logics, property classes, or sizes the method will not cover, and report them honestly.

Claim-to-evidence design table

Verification claim	Matching evidence	Reject pattern avoided
"Procedure is sound/complete"	Theorem + proof; witness + independent checker	"Soundness asserted, never checked"
"Faster than prior tool"	Standard set (pinned), latest baseline, equal limits, cactus+scatter	"Untuned/old baseline; unequal limits"
"Solves instances others cannot"	Those instances run on both tools, at the stated limit	"Only our tool was run on them"
"Scales to large systems"	Runtime/memory across realistic sizes; largest instance stated	"Only small inputs; 'large' undefined"
"General across a theory/domain"	A diverse benchmark sample + explicit out-of-scope classes	"One family, claimed universal"

Fair-comparison checklist (the reviewer's first objections)

[Baseline]   latest released version? documented configuration? cited correctly?
[Limits]     identical per-instance time and memory for all tools? stated hardware and cores?
[Set]        standard benchmark set at a pinned revision? subset justified? instance list archived?
[Accounting] solved/unsolved/timeout/memout/error reported separately, not merged into one number?
[Soundness]  differential check across tools? disagreements reported? witnesses for UNSAT/verified?
[Variance]   for randomized/portfolio runs: seeds fixed, repetitions and variance reported?

Reporting floor

• Report the resource limit with every runtime claim; a speed number without a timeout is meaningless.
• Use cactus and/or scatter plots for multi-instance comparisons; report how many instances each tool uniquely solved.
• State the hardware, core count, and number of runs; note any tool that errored or was excluded and why.

Vignette: evaluating a model-checking technique

Suppose the paper claims a new abstraction lets a model checker verify properties prior tools time out on. The matching plan: draw instances from a standard set at a pinned revision; run the new tool and the strongest prior checker(s), at their latest versions, under one uniform time/memory limit on stated hardware; report a cactus plot and a scatter plot, with solved/timeout/error broken out and the uniquely-solved instances named; differential-check verdicts against a trusted checker; and state the property classes and system sizes out of scope as declared limits — every number traceable to a logged run in the artifact.

Output format

[Evaluation readiness] strong / adequate / weak
[Claim -> evidence map] <claim: benchmark set(revision)/baseline+version/limits, or proof+witness>
[Baseline fairness] <baseline -> latest version? equal limits? documented config?>
[Soundness check] <differential check + witnesses present? yes/no>
[Reporting] <cactus/scatter? solved/timeout/error separated? hardware+seeds stated?>
[Limits-by-design] <logic/property-class/size out of scope -> stated?>
[Decision-critical next run] <one experiment to add or fix>