Agent Skills
› brycewang-stanford/Awesome-Journal-Skills
› cav-experiments
cav-experiments
GitHub用于CAV论文实验设计，强调证据与声明匹配。涵盖基准选择、公平基线对比、超时主导分析、声纳性交叉检查及可视化报告，确保评估公正严谨。
Trigger Scenarios
设计CAV实证评估
审计验证实验
准备CAV论文提交
Install
npx skills add brycewang-stanford/Awesome-Journal-Skills --skill cav-experiments -g -y
SKILL.md
Frontmatter
{
"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>
Version History
- 9f86f09 Current 2026-07-19 14:38
