Cav Review Process

---
name: cav-review-process
description: Use when reasoning about how a CAV (Computer Aided Verification) submission is evaluated, covering the two-stage reviewing process (two reviews then an early-reject filter, then two more reviews with a rebuttal), the partial double-anonymity by category, the accept/reject outcome, the optional non-conditional artifact evaluation, and how CAV differs from TACAS and FMCAD.
---

# CAV Review Process

Model the pipeline before interpreting any single review. CAV's process is a **two-stage filter**:
a paper must survive the first two reviews before it reaches a rebuttal and the second pair of
reviews. The most consequential mental shift for authors arriving from a single-round rebuttal
conference is that **a paper can be rejected before the rebuttal ever happens** — so the first read
has to stand on its own.

## Process model

- Submission and review run on the CAV portal (EasyChair or HotCRP — **verify the live link**) with
  **partial double-anonymity**: Regular and Application papers are anonymized; Short Tool and
  Industrial Experience papers are not.
- **Stage 1:** each paper receives **two** reviews. Papers with sufficient support proceed; the
  rest are **rejected early** (CAV 2026 tentative first-round outcome ~4 Mar 2026).
- **Stage 2:** surviving papers receive **two additional** reviews and an **author-response
  (rebuttal)** window (CAV 2026: 30 Mar - 2 Apr 2026).
- **Outcome:** accept or reject (CAV 2026 notification 17 Apr 2026). Accepted papers publish open
  access in **Springer LNCS**, and authors may then submit an artifact to the AEC on its own
  deadline.
- Reviewers weigh the **significance** of the verification contribution, the **soundness** of the
  technique and its proofs, the **fairness and reproducibility** of the benchmark evaluation, the
  **novelty/delta** against prior verification work, and **clarity** — and see the artifact-intent
  declaration.

## Reading a decision against the stages

| Signal | What it means | Author move |
|---|---|---|
| Early reject after stage 1 | Two reviewers saw a fatal gap (unsound claim, weak evaluation, thin delta) | No rebuttal exists; reframe or reroute (TACAS/FMCAD/VMCAI) — do not resubmit unchanged |
| Passed to stage 2 | The contribution is plausible; specific concerns remain | Use the rebuttal to fix factual misreadings and supply the missing number/proof detail |
| Accept | Contribution, soundness, and evidence hold | Camera-ready + optional artifact; do not reopen scope |
| Reject after stage 2 | A concern the rebuttal did not resolve | Address it substantively before any resubmission |

The strategic reading: write the submission so its **soundness and headline benchmark result are
legible in the first two reviews**. A contribution that only convinces after the rebuttal may never
reach the rebuttal.

## How CAV differs from its siblings

- **vs. TACAS:** TACAS (at ETAPS) overlaps heavily in scope and also values tools, but is a distinct
  venue with its own calendar and process; never assume they share a deadline or a review model.
  CAV's identity is the flagship LNCS proceedings and the two-stage filter.
- **vs. FMCAD:** FMCAD centers formal methods in hardware/design; its review culture and page model
  differ. A hardware-methodology paper may be read as more native there.
- **vs. a single-round rebuttal conference:** the early-reject stage is the key difference — plan for
  it (`cav-workflow`).

## Who reads you

Expect verification-literate reviewers matched to your subarea (model checking, SMT, theorem
proving, program analysis, hardware or NN verification). They check whether the **theorem actually
holds**, whether the **baselines and benchmarks are fair and pinned**, whether the claim is scoped
to what was proved and measured, and — for tool papers — whether the **tool is real and usable**.
Vague algorithm descriptions and unpinned benchmarks get caught, not skimmed.

## Where author leverage actually exists

```text
[Before submission]  category + topic tags -> reviewer pool and page/anonymity rules  (largest lever)
[Stage 1]            nothing to do but wait; the paper must defend itself
[Rebuttal (stage 2)] correct factual misreadings; supply a missing number, proof detail, or
                     benchmark clarification the reviewers can verify
[After reject]       no appeal; reroute to a sibling flagship or a journal (FMSD/JAR)
```

A rebuttal moves borderline papers when it corrects a misreading of a theorem or supplies a
benchmark clarification a reviewer said was missing; it does not move papers when it argues taste or
promises unrun experiments.

## Reading a review packet

Weight reviews before answering. A review that engages your theorem statement, checks your
assumptions, or questions a specific benchmark was read closely and will be read closely again — its
author is your likely advocate if the rebuttal holds. A review that only questions novelty has left
soundness and evaluation to the others; answer each reviewer on the axis they raised. Reviewers
often end with explicit questions; the rebuttal is scored heavily on whether each got a direct,
verifiable answer.

## Misreadings to avoid

- **Treating stage 1 as a formality** — the early-reject filter is real; the first two reviews
  decide whether a rebuttal ever happens.
- **Treating the rebuttal as a debate** — the PC decides; your response is evidence for an advocate,
  not a closing argument.
- **Assuming artifact evaluation gates acceptance** — it is optional and non-conditional at CAV.
- **Projecting a sibling's process** — TACAS and FMCAD have their own models; do not carry them over.

## Output format

```text
[Process stage] pre-submission / stage-1 / rebuttal / final / accepted / artifact
[Outcome so far] early-reject / passed to stage 2 / accept / reject, with the driving criterion
[Criterion map] each review point -> significance | soundness/proof | evaluation | novelty | clarity
[Leverage plan] the next-stage action that can actually change the outcome
[Forbidden moves] identity leak (anonymized categories) / unsupported new claims / unrun promises
```