TACAS Experiments
Use this before submission when the empirical story is not yet locked. TACAS reviewers are
verification experts, and the evaluation is where a tool or algorithm is won or lost. The organizing
principle is honest, reproducible comparison: the experiment must test the claim on shared
benchmarks, against a fairly configured baseline, with every number reproducible in the
artifact (mandatory for tool papers).
Evaluation audit
- Use community benchmarks. Draw tasks from established suites (e.g., SV-COMP task sets, model-
checking or SMT benchmark libraries, prior tool distributions) rather than a private set of
favourable inputs. A benchmark nobody else uses invites the "cherry-picked" reject.
- Configure baselines fairly. Compare against the strongest available competing tool, with a
documented, equal time and memory budget on the same hardware. An untuned or crippled
baseline is a scored weakness, and reviewers often know the baseline's authors.
- Report the right quantities. Solved/unsolved counts, wall-clock time with the timeout stated,
memory, and the largest instance handled — not a single ratio. State the machine (CPU, RAM) and the
number of repetitions for any variance.
- Check your results for soundness. Verification tools can be fast because they are wrong: report
how you validated answers (cross-checking against a reference tool, witness validation, known
expected verdicts), and disclose any incorrect results rather than hiding them.
- Reproduce in the artifact. Every table and figure must regenerate from a script in the artifact
on the clean ETAPS VM; a tool paper whose numbers cannot be reproduced fails the mandatory
artifact evaluation and endangers the paper.
- Bound external validity. Say which languages, property classes, or system sizes the results
cover, and name the ones they do not.
Claim-to-evidence design table
| Verification claim |
Matching evidence |
Reject pattern avoided |
| "Verifies more tasks than prior tools" |
Solved counts on a shared benchmark set vs a tuned baseline, equal timeout |
"Evaluated on our own examples only" |
| "Faster / more scalable" |
Wall-clock and memory across realistic sizes, hardware stated |
"Speedup ratio with no timeout or machine given" |
| "Finds real bugs" |
Reproducible counterexamples/witnesses on real code, validated |
"Warnings with no confirmed true positives" |
| "Sound (or sound up to k)" |
Correctness argument + no incorrect verdicts on a validation set |
"Fast because it silently under-approximates" |
| "General technique" |
Multiple property classes / languages + stated limits |
"One benchmark family, claimed universal" |
Fair-comparison checklist
[Baseline] strongest competitor, latest version, cited; not a straw man
[Budget] identical timeout and memory limit for every tool; state them
[Hardware] one machine, described; note any parallelism and core counts
[Tasks] a named, shared benchmark set; report per-category, not just totals
[Validation] answers cross-checked / witnesses validated; incorrect results disclosed
[Determinism] fix seeds/options; report variance across repetitions where relevant
SV-COMP vs a TACAS tool-paper evaluation
TACAS hosts SV-COMP, but a competition entry and a tool-paper evaluation are different
deliverables — do not conflate them:
- SV-COMP runs your verifier on the common task set under the organizers' harness and rules,
and reports a ranked, uniform comparison across all participants; your contribution is a short
competition paper plus a conforming tool.
- A tool paper is peer-reviewed prose making a specific claim about your tool, evaluated on
benchmarks you justify, judged on contribution and a reproducible artifact — not on a
leaderboard position. You may use SV-COMP benchmarks in a tool paper, but cite them and keep the
comparison fair and reproducible.
Vignette: evaluating a new model checker
Suppose the paper claims a new checker verifies more C tasks than the prior tool. The matching plan:
take a shared C benchmark set (with categories), run both tools with an identical timeout and memory
limit on one stated machine, report per-category solved/unsolved and wall-clock, validate
verdicts (cross-check disagreements, validate violation witnesses), disclose any wrong answers,
state which property classes are out of scope, and ship a clean-VM artifact whose scripts regenerate
every table.
Reporting floor
- Machine description, timeout, and memory limit for every experiment.
- Per-benchmark or per-category results, not only aggregate totals.
- A soundness/validation statement and honest disclosure of incorrect results.
- Artifact scripts that regenerate each table/figure on the ETAPS VM.
Output format
[Evaluation readiness] strong / adequate / weak
[Claim -> evidence map] <claim: benchmark set / metric / baseline>
[Baseline fairness] <baseline -> latest? equal budget? same hardware? documented?>
[Soundness] <validation method; any incorrect results disclosed? yes/no>
[Reproducibility] <every number regenerates on the clean VM? yes/no>
[Decision-critical next run] <one experiment or validation to add>
Source: brycewang-stanford/Awesome-Journal-Skills → TACAS-Skills/skills/tacas-experiments/SKILL.md
1---2name: tacas-experiments3description: Use when designing or auditing a TACAS (ETAPS) evaluation, covering shared verification benchmarks (SV-COMP-style task sets), fair baseline configuration and equal time budgets, honest wall-clock/scalability reporting on stated hardware, soundness checking of results, reproducibility on the clean artifact VM, and how a TACAS tool-paper evaluation differs from a SV-COMP competition entry.4---567# TACAS Experiments89Use this before submission when the empirical story is not yet locked. TACAS reviewers are10verification experts, and the evaluation is where a tool or algorithm is won or lost. The organizing11principle is **honest, reproducible comparison**: the experiment must test the claim on **shared12benchmarks**, against a **fairly configured baseline**, with every number **reproducible in the13artifact** (mandatory for tool papers).1415## Evaluation audit1617- **Use community benchmarks.** Draw tasks from established suites (e.g., SV-COMP task sets, model-18 checking or SMT benchmark libraries, prior tool distributions) rather than a private set of19 favourable inputs. A benchmark nobody else uses invites the "cherry-picked" reject.20- **Configure baselines fairly.** Compare against the **strongest available** competing tool, with a21 **documented, equal time and memory budget** on the **same hardware**. An untuned or crippled22 baseline is a scored weakness, and reviewers often know the baseline's authors.23- **Report the right quantities.** Solved/unsolved counts, wall-clock time with the **timeout stated**,24 memory, and the largest instance handled — not a single ratio. State the machine (CPU, RAM) and the25 number of repetitions for any variance.26- **Check your results for soundness.** Verification tools can be fast because they are wrong: report27 how you validated answers (cross-checking against a reference tool, witness validation, known28 expected verdicts), and disclose any incorrect results rather than hiding them.29- **Reproduce in the artifact.** Every table and figure must regenerate from a script in the artifact30 on the **clean ETAPS VM**; a tool paper whose numbers cannot be reproduced fails the mandatory31 artifact evaluation and endangers the paper.32- **Bound external validity.** Say which languages, property classes, or system sizes the results33 cover, and name the ones they do not.3435## Claim-to-evidence design table3637| Verification claim | Matching evidence | Reject pattern avoided |38|---|---|---|39| "Verifies more tasks than prior tools" | Solved counts on a shared benchmark set vs a tuned baseline, equal timeout | "Evaluated on our own examples only" |40| "Faster / more scalable" | Wall-clock and memory across realistic sizes, hardware stated | "Speedup ratio with no timeout or machine given" |41| "Finds real bugs" | Reproducible counterexamples/witnesses on real code, validated | "Warnings with no confirmed true positives" |42| "Sound (or sound up to k)" | Correctness argument + no incorrect verdicts on a validation set | "Fast because it silently under-approximates" |43| "General technique" | Multiple property classes / languages + stated limits | "One benchmark family, claimed universal" |4445## Fair-comparison checklist4647```text48[Baseline] strongest competitor, latest version, cited; not a straw man49[Budget] identical timeout and memory limit for every tool; state them50[Hardware] one machine, described; note any parallelism and core counts51[Tasks] a named, shared benchmark set; report per-category, not just totals52[Validation] answers cross-checked / witnesses validated; incorrect results disclosed53[Determinism] fix seeds/options; report variance across repetitions where relevant54```5556## SV-COMP vs a TACAS tool-paper evaluation5758TACAS **hosts SV-COMP**, but a competition entry and a tool-paper evaluation are different59deliverables — do not conflate them:6061- **SV-COMP** runs your verifier on the **common task set** under the organizers' harness and rules,62 and reports a ranked, uniform comparison across all participants; your contribution is a short63 competition paper plus a conforming tool.64- **A tool paper** is peer-reviewed prose making a **specific claim** about your tool, evaluated on65 benchmarks *you* justify, judged on contribution and a reproducible artifact — not on a66 leaderboard position. You may *use* SV-COMP benchmarks in a tool paper, but cite them and keep the67 comparison fair and reproducible.6869## Vignette: evaluating a new model checker7071Suppose the paper claims a new checker verifies more C tasks than the prior tool. The matching plan:72take a shared C benchmark set (with categories), run both tools with an identical timeout and memory73limit on one stated machine, report per-category solved/unsolved and wall-clock, **validate**74verdicts (cross-check disagreements, validate violation witnesses), disclose any wrong answers,75state which property classes are out of scope, and ship a clean-VM artifact whose scripts regenerate76every table.7778## Reporting floor7980- Machine description, timeout, and memory limit for every experiment.81- Per-benchmark or per-category results, not only aggregate totals.82- A soundness/validation statement and honest disclosure of incorrect results.83- Artifact scripts that regenerate each table/figure on the ETAPS VM.8485## Output format8687```text88[Evaluation readiness] strong / adequate / weak89[Claim -> evidence map] <claim: benchmark set / metric / baseline>90[Baseline fairness] <baseline -> latest? equal budget? same hardware? documented?>91[Soundness] <validation method; any incorrect results disclosed? yes/no>92[Reproducibility] <every number regenerates on the clean VM? yes/no>93[Decision-critical next run] <one experiment or validation to add>94```9596---9798**Source:** [`brycewang-stanford/Awesome-Journal-Skills`](https://github.com/brycewang-stanford/Awesome-Journal-Skills) → `TACAS-Skills/skills/tacas-experiments/SKILL.md`
thedixitjain