Tacas writing style

TACAS Writing Style

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.

Revision rules (all categories)

• Lead with the construction/analysis problem and the contribution. State what the paper builds or decides, on what inputs, and how — before any adjective. A verification reader wants the object of study (a property, a system model, a decision problem) named immediately.
• State the soundness claim explicitly. "Sound," "sound and complete," "complete up to bound k," or "unsound but effective, and here is why that is acceptable" — say which, and point to the argument. An unstated correctness posture is the first thing a TACAS reviewer probes.
• Pair every empirical claim with honest evidence — named benchmarks, a fair baseline, wall-clock time on stated hardware, and solved/unsolved counts — not "outperforms."
• Match structure to category. A research paper foregrounds the algorithm and its proof; a tool paper foregrounds the tool, its architecture, and its artifact; a case study foregrounds the system and the lessons; a tool-demo foregrounds a reproducible demonstration in six pages.
• Respect the page budget as a design constraint. 16 pages (or 6 for a tool-demo) in llncs.cls, excluding references and appendix — a contribution that only fits by compressing the soundness argument is over-scoped for the category.
• For a research (double-blind) paper, maintain anonymity in prose: third-person self-citation, no tool name that identifies you, no identifying acknowledgements. A tool/case-study paper is single-blind and names itself.

Category skeletons

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

Sentence-level rewrites

Draft pattern	TACAS-safe rewrite
"Our tool is very efficient and novel."	"solves N/120 benchmarks vs M/120 for <baseline>, median 3.1x less wall-clock time (same hardware, equal timeout)"
"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 <named baseline> configured with an equal time budget, on <named benchmark set>"
"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 <benchmark set> (N tasks); results, hardware, and timeouts are in §4 and the artifact"

Soundness-and-evidence discipline

[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

Vignette: compressing a research paper to 16 pages

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.

Output format

[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>