CAV Related Work

CAV Related Work

Use this to audit novelty and eligibility. CAV reviewers are close to the verification literature and expect to see where your paper sits relative to the nearest prior technique or tool — stated as a delta, not a list. Reopen the current CFP for dual-submission, anonymity, and prior-publication rules before advising authors.

Positioning checks

• Separate the verification novelty from the engineering effort. What is new: an algorithm, a decision procedure, an abstraction, a soundness result, a tool capability, or a benchmark regime nobody had covered?
• Cover the verification lanes. CAV reviewers expect the flagship venues, the tool ecosystems, and the journals — not just the papers nearest your method (see the table). A bibliography missing the obvious sibling work reads as unaware.
• Write delta-first. Each closely related paper gets one sentence naming what it did and one naming what you do differently — a technical contrast (what their method cannot do that yours can), not a summary.
• Credit tool and benchmark lineages. If you extend or compare against a solver/model checker or use a standard benchmark set, cite the tool paper and the benchmark/competition to their real origin — and to the right venue (Z3 is TACAS, not CAV; see the exemplars guardrails).
• Preserve double-anonymity where required. For Regular and Application papers, cite your own prior work in the third person and never link reviewers to an identity-revealing preprint, repository, or tool homepage. (Tool and Industrial papers are not anonymized.)
• Declare overlap with any prior workshop/conference version or concurrent submission; do not re-submit archival work as new.

Verification literature lanes

A bibliography that cites only your own subarea tells a reviewer the delta may be smaller than claimed; one that reaches the sibling flagships, the tool papers, and the journals signals command of