Use this when revising the main paper. TACAS papers are LNCS articles read by verification experts, so they need the contribution stated precisely on the first page and claims a reviewer can check — a soundness argument for a research paper, a working tool with reproducible numbers for a tool paper. The failure this skill prevents is a paper that gestures at "efficiency" and "novelty" without a crisp algorithmic claim or an honest evaluation.
llncs.cls,
excluding references and appendix — a contribution that only fits by compressing the soundness
argument is over-scoped for the category.| Category | First-page job | Backbone sections | Common failure |
|---|---|---|---|
| Research | Problem, algorithm, soundness claim, evidence preview | Preliminaries; algorithm; correctness; evaluation | Leads with a trend, hides the algorithm and its guarantee |
| Regular tool | What the tool does, how, availability | Architecture; technique realized; evaluation on benchmarks; artifact | Adjectives instead of an architecture and a fair comparison |
| Case study | The real system and the question | System; method applied; results; lessons and threats | Anecdote instead of transferable, honestly bounded lessons |
| Tool-demo | A concrete demonstration in 6 pages | What is shown; how a user drives it; what is reproducible | Compressed research paper instead of a genuine demonstration |
| Draft pattern | TACAS-safe rewrite |
|---|---|
| "Our tool is very efficient and novel." | "solves N/120 benchmarks vs M/120 for |
| "We prove the approach is correct." | "Theorem 1: the encoding is sound and complete up to bound k (proof in §3.2 / appendix)" |
| "We outperform existing approaches." | "against |
| "The tool scales well." | "runtime grows sub-linearly to inputs of 10^6 states; the largest solved instance is stated in Table 2" |
| "Extensive experiments show..." | "we evaluate on |
[Guarantee] sound? complete? bounded? unsound-but-useful? -> state it and cite the argument
[Baseline] the strongest available tool, configured fairly, on the same benchmarks and hardware
[Reporting] solved/unsolved, wall-clock with timeouts, memory; no single hidden headline ratio
[Reproduce] every reported number traces to a script/log in the artifact (mandatory for tools)
-> place the guarantee near the algorithm and the evidence near the claim it supports
A draft with a full proof, three optimizations, and a sprawling background: keep the algorithm, the soundness theorem with a proof sketch (full proof to the appendix), the one optimization that carries the speedup, and the benchmark comparison; move the secondary optimizations and extended proofs to the appendix with forward references; cut background to what the argument needs. The test of a good cut: a reviewer can state your guarantee and reproduce your headline benchmark result from the body alone.
[Writing diagnosis] clear / under-specified / over-claimed / evidence-thin / wrong-category-shape
[First-page fix] <new framing: problem -> contribution -> guarantee -> evidence>
[Guarantee audit] <soundness/completeness/bound stated? where argued?>
[Evidence audit] <claim -> benchmark -> baseline -> fair? reproducible? yes/no>
[Anonymity edits] (research only) <tool names / self-citations / acks to rewrite>