CAV Writing Style

CAV Writing Style

Use this when revising the main paper. CAV papers are Springer LNCS chapters read by verification researchers, so they need a precise verification contribution stated on the first page and a formal guarantee a reviewer can check. The failure this skill prevents is a technically fine paper that reads like a systems demo or a heuristic with a benchmark table but no stated property.

Revision rules

• Lead with the verification contribution and its guarantee: the problem (what property, of what system), why current methods fall short, the contribution (technique and/or tool), what is formally guaranteed (soundness, completeness, an equisatisfiability/refinement claim), the benchmark evidence, and the scope.
• State the formal claim precisely. Name the property, the assumptions, and the theorem. A paper whose "contribution" is only "faster on benchmarks" with no guarantee reads as a tool note, not a Regular Paper.
• Give proofs their place. Key proofs go in the body; long proofs may go to a clearly-marked appendix — but reviewers are not obliged to read appendices, so the proof idea must be in the body (see cav-supplementary).
• Make benchmark claims falsifiable. Every empirical claim names the benchmark set (with revision), the baseline tools and versions, and the resource limits (time/memory) — adjectives like "significantly faster" without these are not evidence (see cav-experiments).
• State scope and limits as your own, not as a closing apology. Say which logics, system sizes, or property classes the method covers and where it stops. Over-claimed generality is the fastest way to lose a verification reviewer's trust.
• Maintain double-blind wording for Regular and Application papers: anonymize self-citations, the tool/solver name, benchmark paths, acknowledgements, and repository links. (Tool and Industrial papers are not anonymized.)

Verification-paper skeleton