TACAS Topic Selection

Decide two things before drafting: is this TACAS, and which TACAS category. TACAS — Tools and Algorithms for the Construction and Analysis of Systems — is the ETAPS conference at the tool-and-algorithm end of verification: model checking, program analysis, SMT and decision procedures, testing and synthesis, and the systems that implement them. Its defining feature versus its siblings is that a usable, evaluated tool is a first-class contribution, backed by a mandatory artifact. A brilliant idea with no tool and no experiment can still be a research paper, but a paper that is really a benchmark ranking is a SV-COMP contribution, not a TACAS paper.

First cut: is this TACAS, or a sibling?

TACAS overlaps heavily with the other verification venues, so decide by emphasis and calendar, not by topic alone.

CAV is the trap. Many canonical tools (NuSMV, CPAchecker, Storm) debuted at CAV, not TACAS. Differentiate by TACAS's ETAPS context, its tool/tool-demo/case-study categories, its per-category page limits, and its artifact-as-first-class model — and check dblp before assuming a lineage.

Second cut: which of the four categories?

The category is a commitment: a research paper is judged on the idea and its soundness; a tool paper is judged on the tool and its runnable artifact; a case-study paper is judged on the realism of the system and the honesty of the lessons; a tool-demo is judged on a working demonstration in six pages. Pick the one whose bar your evidence actually clears.

Contribution shapes TACAS rewards

• Algorithm / reduction — a new way to construct or analyse systems with a soundness (and often completeness/complexity) argument (the BMC lineage).
• Tool — a downloadable, evaluated implementation others can point at their own inputs (the CBMC / Z3 lineage), now inseparable from a working artifact.
• Case study — a substantial application of verification to a real system that teaches the community what works and what breaks at scale.
• Competition-driven — participation in SV-COMP / VerifyThis that advances shared benchmarks and reproducible comparison.

The tool-vs-research and re-label tests

• Tool-vs-research test: if the paper's core would survive with the tool removed (an algorithm and a proof), it is a research paper; if the core is the working tool and its evaluation, it is a tool paper — and then the artifact is mandatory.
• Re-label test: could this be submitted to CAV/VMCAI/FMCAD unchanged and read as native there? If its heart is FM breadth or new theory depth, weigh those venues; TACAS rewards the tool-and-algorithm framing with reproducible experiments.

Cheap reconnaissance before committing

[Scope]   scan the last two TACAS proceedings (dblp, Springer LNCS) for your subarea
          -> several recent papers = a reviewer pool exists; none = mismatch or a CAV/FMCAD topic
[Category] find 2-3 recent papers in the category you plan to use; match their evidence depth
[Artifact] if tool/tool-demo, can you package a clean-VM artifact by the post-paper deadline? if
          not, the category is wrong for this cycle
[Calendar] compare the next ETAPS/TACAS deadline with CAV/VMCAI/FMCAD dates -> route to the
          nearest honest fit rather than idling a year

Decision procedure

[Is it TACAS?] tool/algorithm to construct/analyse systems + experiments? -> yes; else CAV/VMCAI/FMCAD/journal
[Competition?] a verifier to be ranked on common tasks -> SV-COMP, not a tool paper
[Category] algorithm+proof -> research; usable tool+eval -> regular tool; mature tool in use -> tool-demo;
          real-system application -> case-study
[Blind + artifact] research -> double-blind, voluntary artifact; tool/tool-demo -> single-blind, mandatory artifact
[Verdict] TACAS <category> / sibling venue / SV-COMP / journal, with a one-line reason

Run this before the writing skills; a wrong venue-or-category decision wastes every later step. When the verdict is TACAS, continue with tacas-workflow for the calendar and tacas-writing-style for the paper shape.