| name | cav-supplementary |
| description | Use when deciding what belongs in a CAV (Computer Aided Verification) paper body versus its optional appendix and artifact, covering the LNCS page limits, the rule that reviewers are not obliged to read the appendix so decision-critical content stays in the body, where full proofs and benchmark tables live, and double-anonymous supplementary material for the anonymized categories. |
CAV Supplementary
Use this when assembling CAV supplementary material. The governing rule is strict and specific to
CAV's format: a clearly marked appendix is allowed, but reviewers are not obliged to read it. So
the paper must be judgeable from the body alone — anything a reviewer must see to accept lives
inside the page limit, and the appendix and artifact only support it.
What goes where
| Content | Body (within the page limit) | Appendix / artifact |
|---|
| The problem, the technique, the main theorem | Yes | — |
| Proof idea / sketch of the main result | Yes | Full formal proof |
| Supporting lemmas | Statement + role | Full proofs |
| Headline benchmark comparison + resource limits | Yes | Full per-instance tables |
| Soundness/differential-check result | The result + method | The raw logs and witnesses |
| Benchmark set + selection | Summary + revision | The full instance list, fetch scripts |
| Tool build/run instructions | A pointer | README + scripts (artifact) |
| Proof certificates / witnesses | A pointer | The certificates + a checker (artifact) |
If a reviewer would need to open the appendix or artifact to know whether the theorem holds or the
comparison is fair, the paper is mis-partitioned — move that content into the body.
The page-limit discipline
CAV's LNCS limits (Regular 18 pages; Short Tool / Application / Industrial 10 pages) exclude
references and appendices, but the appendix is optional-to-read. Consequences:
- Keep the main theorem's proof idea and the headline benchmark result with its resource
limits in the body — they are decision-critical.
- Move full formal proofs, per-instance benchmark tables, and extra property classes to
the appendix or artifact with explicit forward references.
- Do not use the appendix to smuggle in a result that would not fit — an argument that only
closes with unread material reads as unreviewable, and the stage-1 filter is unforgiving.
Double-anonymous supplementary rules (Regular and Application papers)
[No identity] no authors, affiliations, acknowledgements, grants, cluster paths, or repo owners in
the appendix or the review-time artifact; anonymize the tool/solver name
[Anonymized links] the artifact link points at an anonymizing host, not a personal repo or tool site
[Clean archive] no .git history, .DS_Store, credentials, caches, or large irrelevant files
[Opens clean] verify the archive unpacks and the README orients a reviewer in minutes on a fresh
machine (the AEC smoke test mirrors this)
Tool and Industrial papers are not anonymized, so their supplementary material may name the tool —
but should still be clean and self-orienting.
Appendix architecture
- Order appendix sections to mirror the paper: main-theorem proof first, then lemma proofs, then full
benchmark tables, then extra experiments — reviewers navigate by the claim, not by page number.
- Keep each appendix section referenced from the body at least once; orphaned material is invisible
under discretionary reading.
- Confirm on the current CFP that appendices are inside the same PDF (not a separate upload) and that
they do not count against the limit — this is the CAV norm but re-verify.
Vignette: splitting a technique-plus-tool paper
A Regular Paper with one main soundness theorem, three lemmas, and a large benchmark study: the body
keeps the problem, the technique, the main theorem with its proof idea, the lemma statements, and the
headline cactus/scatter comparison with the resource limits and the soundness cross-check; the
appendix holds the full proofs; the artifact holds the pinned benchmark set, the per-instance logs,
the seeds, the proof witnesses with a checker, and the reproduction scripts. Nothing decision-critical
lives only in unread material, because the stage-1 reviewers judge from the body.
Output format
[Supplement status] ready / needs fixes / not ready
[Partition check] anything decision-critical outside the body? <none / move: what>
[Page limit] body within the category limit? appendix marked and referenced? yes/no
[Anonymity] appendix + review artifact clean of identity (Regular/Application)? passed/issues
[Body dependency] <what a reviewer can decide without opening the appendix/artifact>
