ICALP Experiments (proof strategy, and computation in service of proofs)

At ICALP there is usually no experiment section — the evidence for the claim is the proof. This skill is therefore about matching the argument to the claim shape, and about the narrow, real cases where computation supports a theorem (a computer-assisted proof, an SMT-checked base case, an exhaustive small-case verification). It is deliberately not an empirical-evaluation guide: a paper whose contribution is a benchmark result is mis-routed (icalp-topic-selection).

Match the argument to the claim

When computation legitimately supports a theorem

Some ICALP results genuinely rely on computation. It must be rigorous and checkable, not suggestive:

• Exhaustive small-case verification — checking a property for all objects up to size k as a base case of an induction. State the exact range, the encoding, and make the search reproducible.
• SAT/SMT-certified steps — using a solver to verify a finite gadget or unsatisfiability. Ship the encoding and, where possible, an independently checkable certificate (UNSAT proof, Farkas witness), not just "the solver said so."
• Computer-assisted case analysis — a program enumerating cases in a proof. The program is part of the proof; its logic must be described and its output verifiable.

The bar: a referee (or a reader of the full version) must be able to re-run or independently check the computation. A number a solver produced with no reproducible input is not a proof step.

Keep it a proof paper, not an experiment paper

• Supporting computation certifies a step; it does not replace the theorem. If the only evidence for the main claim is "it worked on our instances," the paper is experimental and belongs elsewhere.
• Do not add a benchmark table to a theory paper to look more complete — ICALP referees read it as either irrelevant or as a signal the theorem is weak.
• Running time measured is not running time proved. The contribution is the provable bound.

Reproducibility of the computational part

If computation backs a proof, treat it like the full version (see icalp-reproducibility):

• Provide the code and inputs (or precise pseudocode) in the appendix / full version or a public repository referenced at camera-ready.
• Provide certificates an independent checker can verify where the technique allows.
• Pin versions (solver, seed if randomized search) so the check is deterministic.

Worked vignette: a dichotomy with a computer-checked base

A Track B paper proves a dichotomy over a family of constraint languages: tractable vs NP-hard. The inductive step is by hand; the base cases (finitely many small languages) are verified by an exhaustive program. To meet the bar: state the finite base set precisely, describe the enumeration, ship the code and its output in the full version, and — for the hardness base cases — include reductions a referee can check by hand rather than leaving them to the program alone. State clearly which cases are machine-verified and which are proved analytically.

Output format

[Claim shape] upper / approximation / lower (uncond) / lower (conditional) / decidability / dichotomy
[Argument fit] the proof strategy matches the claim? gaps: <where>
[Computation role] none / base-case check / solver-certified step / computer-assisted cases
[Checkability] certificate or reproducible input provided? independent check possible? yes/no
[Not-an-experiment guard] is the theorem the evidence (not benchmark performance)? yes/no
[Fix queue] <ordered: proof gaps, missing certificates, mis-routed empirical framing>