CAV Author Response

CAV Author Response

Use this after CAV stage-2 reviews are released. At CAV the rebuttal exists only for papers that passed the stage-1 filter — the two-stage process means a rejected paper never reaches this turn. So the rebuttal is a focused instrument: answer what the two additional reviewers, and the two from stage 1, need in order to advocate for the paper in the PC discussion. For Regular and Application papers, the response must respect double-anonymity — do not reveal authors, the tool's real name, or identity-revealing repositories.

Triage

• Answer what affects the decision: soundness of the theorem/proof, fairness and reproducibility of the benchmarks, novelty/delta against prior verification work, scope, and clarity.
• Use evidence that already exists in the submission or that you can state precisely — a proof step, a number already in a table, a benchmark-configuration clarification. Do not promise unrun experiments as if they were results.
• Correct factual misreadings first; a reviewer who misread a theorem's assumption or a benchmark subset is often persuadable.
• Keep every word anonymous for anonymized categories. (Tool and Industrial papers are not double-blind, so this constraint relaxes — but still avoid gratuitous self-promotion.)

The verification rebuttal, point by point

Treat the response as a claim ledger: for each reviewer concern, either resolve it with concrete evidence or explain precisely why the concern does not apply.

[R1.1] "The soundness proof assumes X, which fails for unbounded inputs."
       -> Response: X is not assumed; Lemma 2 holds for unbounded inputs (the bound is only on
          the encoding width, §3.2). Pointer: §3.2, Lemma 2.
[R2.1] "The baseline solver was not the latest version / not tuned."
       -> Response: baseline is vA.B (latest release at submission); we used its default portfolio
          as recommended in its README; per-instance data in the artifact confirms parity of limits.
[R2.2] "Novelty over <prior technique> is unclear."
       -> Response: prior technique shares lemmas only propositionally; ours admits theory lemmas
          under a re-derivation check (the soundness contribution), see §3.3 and Table 2.

The rule that turns a stage-2 paper into an acceptance: **answer the axis the reviewer raised, with