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

| 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>