Cav Supplementary

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

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>