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 , 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 configured with an equal time budget, on " |
| "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 (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>
1---2name: tacas-writing-style3description: Use when revising a TACAS (ETAPS) paper for a clear construction-or-analysis contribution on the first page, a stated soundness/completeness claim, honest benchmark evidence, category-appropriate structure (research vs tool vs case-study vs tool-demo), disciplined use of the 16-page (or 6-page) LNCS budget, and correct handling of double-blind wording for research papers.4---56# TACAS Writing Style78Use this when revising the main paper. TACAS papers are LNCS articles read by verification experts,9so they need the **contribution stated precisely on the first page** and **claims a reviewer can10check** — a soundness argument for a research paper, a working tool with reproducible numbers for a11tool paper. The failure this skill prevents is a paper that gestures at "efficiency" and "novelty"12without a crisp algorithmic claim or an honest evaluation.1314## Revision rules (all categories)1516- **Lead with the construction/analysis problem and the contribution.** State what the paper builds17 or decides, on what inputs, and how — before any adjective. A verification reader wants the object18 of study (a property, a system model, a decision problem) named immediately.19- **State the soundness claim explicitly.** "Sound," "sound and complete," "complete up to bound20 *k*," or "unsound but effective, and here is why that is acceptable" — say which, and point to the21 argument. An unstated correctness posture is the first thing a TACAS reviewer probes.22- **Pair every empirical claim with honest evidence** — named benchmarks, a fair baseline, wall-clock23 time on stated hardware, and solved/unsolved counts — not "outperforms."24- **Match structure to category.** A research paper foregrounds the algorithm and its proof; a tool25 paper foregrounds the tool, its architecture, and its artifact; a case study foregrounds the26 system and the lessons; a tool-demo foregrounds a reproducible demonstration in six pages.27- **Respect the page budget as a design constraint.** 16 pages (or 6 for a tool-demo) in `llncs.cls`,28 excluding references and appendix — a contribution that only fits by compressing the soundness29 argument is over-scoped for the category.30- **For a research (double-blind) paper, maintain anonymity in prose:** third-person self-citation,31 no tool name that identifies you, no identifying acknowledgements. A tool/case-study paper is32 single-blind and names itself.3334## Category skeletons3536| Category | First-page job | Backbone sections | Common failure |37|---|---|---|---|38| Research | Problem, algorithm, soundness claim, evidence preview | Preliminaries; algorithm; correctness; evaluation | Leads with a trend, hides the algorithm and its guarantee |39| Regular tool | What the tool does, how, availability | Architecture; technique realized; evaluation on benchmarks; artifact | Adjectives instead of an architecture and a fair comparison |40| Case study | The real system and the question | System; method applied; results; lessons and threats | Anecdote instead of transferable, honestly bounded lessons |41| 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 |4243## Sentence-level rewrites4445| Draft pattern | TACAS-safe rewrite |46|---|---|47| "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)" |48| "We prove the approach is correct." | "Theorem 1: the encoding is sound and complete up to bound k (proof in §3.2 / appendix)" |49| "We outperform existing approaches." | "against <named baseline> configured with an equal time budget, on <named benchmark set>" |50| "The tool scales well." | "runtime grows sub-linearly to inputs of 10^6 states; the largest solved instance is stated in Table 2" |51| "Extensive experiments show..." | "we evaluate on <benchmark set> (N tasks); results, hardware, and timeouts are in §4 and the artifact" |5253## Soundness-and-evidence discipline5455```text56[Guarantee] sound? complete? bounded? unsound-but-useful? -> state it and cite the argument57[Baseline] the strongest available tool, configured fairly, on the same benchmarks and hardware58[Reporting] solved/unsolved, wall-clock with timeouts, memory; no single hidden headline ratio59[Reproduce] every reported number traces to a script/log in the artifact (mandatory for tools)60-> place the guarantee near the algorithm and the evidence near the claim it supports61```6263## Vignette: compressing a research paper to 16 pages6465A draft with a full proof, three optimizations, and a sprawling background: keep the algorithm, the66soundness theorem with a proof sketch (full proof to the appendix), the one optimization that67carries the speedup, and the benchmark comparison; move the secondary optimizations and extended68proofs to the appendix with forward references; cut background to what the argument needs. The test69of a good cut: a reviewer can state your guarantee and reproduce your headline benchmark result from70the body alone.7172## Output format7374```text75[Writing diagnosis] clear / under-specified / over-claimed / evidence-thin / wrong-category-shape76[First-page fix] <new framing: problem -> contribution -> guarantee -> evidence>77[Guarantee audit] <soundness/completeness/bound stated? where argued?>78[Evidence audit] <claim -> benchmark -> baseline -> fair? reproducible? yes/no>79[Anonymity edits] (research only) <tool names / self-citations / acks to rewrite>80```
brycewang-stanford