TACAS Related Work
Use this to audit novelty and eligibility. TACAS reviewers are close to the verification literature
and to the tools it produces, so they expect to see where your algorithm or tool sits relative to
the nearest prior work — as a delta, not a catalog. Reopen the current call for dual-submission,
anonymity, and prior-publication rules before advising authors.
Positioning checks
- Separate the algorithmic novelty from the engineering. What is new: a new decision procedure,
a new encoding, a new abstraction, a tool that first makes a technique usable, or a case study
that first applies it at scale? Name it precisely.
- Cover the verification venues. TACAS reviewers expect the flagships and the journals, not just
the papers nearest your method (see the table). Missing the obvious CAV/VMCAI/FMCAD predecessor
reads as unaware.
- Credit what you build on. If you use an SMT solver, a benchmark suite, or a model-checking
backend, cite it — TACAS is a tool-and-algorithm community and reviewers notice uncredited
infrastructure or benchmarks.
- Write delta-first. Each closely related tool/algorithm gets one sentence on what it did and one
on what you do differently (a stronger guarantee, a new class handled, an order-of-magnitude
scaling, a first working tool) — not a summary.
- Anonymity by category. For a double-blind research paper, cite your own prior work in the
third person and never link reviewers to an identity-revealing preprint or repository. A tool /
case-study paper is single-blind and cites itself normally.
- Declare overlap with any prior workshop version, SV-COMP competition paper, or concurrent
submission; do not re-submit archival work as new.
Verification literature lanes
| Lane |
Typical venues |
What TACAS reviewers check |
| Tools & algorithms (home) |
TACAS |
Whether the nearest tool/algorithm predecessor is compared or distinguished |
| Broad formal methods |
CAV |
Whether the closest FM-flagship technique is credited and contrasted |
| Verification / abstract interpretation foundations |
VMCAI |
Whether the foundational predecessor is engaged |
| Hardware / SAT-centric FM |
FMCAD |
Whether the relevant hardware/SAT lineage is acknowledged |
| Explicit-state / software model checking |
SPIN |
Whether the model-checking predecessor is cited |
| Journals |
STTT, FMSD |
Whether deeper journal treatments on the topic are engaged |
| Competitions |
SV-COMP, VerifyThis |
Whether shared benchmarks / competing verifiers are credited |
A bibliography that cites only your own subarea suggests the delta is smaller than claimed; one that
reaches the flagships, journals, and competitions signals command of the field.
Delta-first positioning vignette
Suppose the paper presents a new tool for bounded refinement checking. Its nearest neighbors: a
CAV algorithm that requires linearization-point annotations (yours is annotation-free), a TACAS tool
that enumerates histories without reduction (yours uses an SMT reduction and scales further), and a
journal study characterizing the problem (no tool). The novelty sentence should name all three
contrasts — annotation-free where prior work needed annotations, an SMT reduction where prior work
enumerated, and a working, benchmarked tool where the journal offered only characterization.
Concurrent and prior-version judgment calls
[SV-COMP competition paper] your tool's competition entry is often citable but archival-limited;
state what the TACAS paper adds beyond the competition contribution
[Concurrent arXiv work] cite neutrally, state the technical difference, avoid priority claims;
keep the citation anonymous for a double-blind research paper
[Prior workshop version] usually citable; declare the overlap and state what the full paper adds
[Prior tool release] crediting your own earlier tool version is fine (single-blind tool paper);
for a research paper, keep it third-person
Eligibility red flags
- Substantial text overlap with a published paper by the same authors (self-plagiarism risk).
- A "new" tool paper that re-reports a prior release's benchmarks without a new capability.
- Citations only to non-verification venues, signaling the paper may be a visitor better suited to
another community and not reframed.
Output format
[Eligibility] clear / needs declaration / risky
[Lanes covered] <TACAS / CAV / VMCAI / FMCAD / SPIN / journals / competitions>
[Nearest 3 works] <work -> one-line delta>
[Infrastructure credited] <solvers / benchmarks / backends cited? yes/no>
[Archival-overlap risk] <none / declare: what (incl. SV-COMP entry)>
[Novelty sentence] <TACAS-ready contribution contrast against the nearest tools/algorithms>
Source: brycewang-stanford/Awesome-Journal-Skills → TACAS-Skills/skills/tacas-related-work/SKILL.md
1---2name: tacas-related-work3description: Use when positioning a TACAS (ETAPS) submission against the verification literature across TACAS, CAV, VMCAI, FMCAD, SPIN, and journals (STTT, FMSD), writing delta-first contrast against the nearest tools and algorithms, crediting the benchmarks and solvers you build on, keeping self-citations anonymous for double-blind research papers, and handling competition-tool and prior-version overlap.4---567# TACAS Related Work89Use this to audit novelty and eligibility. TACAS reviewers are close to the verification literature10and to the tools it produces, so they expect to see where your algorithm or tool sits relative to11the nearest prior work — as a **delta**, not a catalog. Reopen the current call for dual-submission,12anonymity, and prior-publication rules before advising authors.1314## Positioning checks1516- **Separate the algorithmic novelty from the engineering.** What is new: a new decision procedure,17 a new encoding, a new abstraction, a tool that first makes a technique usable, or a case study18 that first applies it at scale? Name it precisely.19- **Cover the verification venues.** TACAS reviewers expect the flagships and the journals, not just20 the papers nearest your method (see the table). Missing the obvious CAV/VMCAI/FMCAD predecessor21 reads as unaware.22- **Credit what you build on.** If you use an SMT solver, a benchmark suite, or a model-checking23 backend, cite it — TACAS is a tool-and-algorithm community and reviewers notice uncredited24 infrastructure or benchmarks.25- **Write delta-first.** Each closely related tool/algorithm gets one sentence on what it did and one26 on what you do differently (a stronger guarantee, a new class handled, an order-of-magnitude27 scaling, a first working tool) — not a summary.28- **Anonymity by category.** For a **double-blind research** paper, cite your own prior work in the29 third person and never link reviewers to an identity-revealing preprint or repository. A **tool /30 case-study** paper is single-blind and cites itself normally.31- **Declare overlap** with any prior workshop version, SV-COMP competition paper, or concurrent32 submission; do not re-submit archival work as new.3334## Verification literature lanes3536| Lane | Typical venues | What TACAS reviewers check |37|---|---|---|38| Tools & algorithms (home) | **TACAS** | Whether the nearest tool/algorithm predecessor is compared or distinguished |39| Broad formal methods | **CAV** | Whether the closest FM-flagship technique is credited and contrasted |40| Verification / abstract interpretation foundations | **VMCAI** | Whether the foundational predecessor is engaged |41| Hardware / SAT-centric FM | **FMCAD** | Whether the relevant hardware/SAT lineage is acknowledged |42| Explicit-state / software model checking | **SPIN** | Whether the model-checking predecessor is cited |43| Journals | **STTT, FMSD** | Whether deeper journal treatments on the topic are engaged |44| Competitions | **SV-COMP, VerifyThis** | Whether shared benchmarks / competing verifiers are credited |4546A bibliography that cites only your own subarea suggests the delta is smaller than claimed; one that47reaches the flagships, journals, and competitions signals command of the field.4849## Delta-first positioning vignette5051Suppose the paper presents a new **tool** for bounded refinement checking. Its nearest neighbors: a52CAV algorithm that requires linearization-point annotations (yours is annotation-free), a TACAS tool53that enumerates histories without reduction (yours uses an SMT reduction and scales further), and a54journal study characterizing the problem (no tool). The novelty sentence should name all three55contrasts — annotation-free where prior work needed annotations, an SMT reduction where prior work56enumerated, and a working, benchmarked tool where the journal offered only characterization.5758## Concurrent and prior-version judgment calls5960```text61[SV-COMP competition paper] your tool's competition entry is often citable but archival-limited;62 state what the TACAS paper adds beyond the competition contribution63[Concurrent arXiv work] cite neutrally, state the technical difference, avoid priority claims;64 keep the citation anonymous for a double-blind research paper65[Prior workshop version] usually citable; declare the overlap and state what the full paper adds66[Prior tool release] crediting your own earlier tool version is fine (single-blind tool paper);67 for a research paper, keep it third-person68```6970## Eligibility red flags7172- Substantial text overlap with a published paper by the same authors (self-plagiarism risk).73- A "new" tool paper that re-reports a prior release's benchmarks without a new capability.74- Citations only to non-verification venues, signaling the paper may be a visitor better suited to75 another community and not reframed.7677## Output format7879```text80[Eligibility] clear / needs declaration / risky81[Lanes covered] <TACAS / CAV / VMCAI / FMCAD / SPIN / journals / competitions>82[Nearest 3 works] <work -> one-line delta>83[Infrastructure credited] <solvers / benchmarks / backends cited? yes/no>84[Archival-overlap risk] <none / declare: what (incl. SV-COMP entry)>85[Novelty sentence] <TACAS-ready contribution contrast against the nearest tools/algorithms>86```8788---8990**Source:** [`brycewang-stanford/Awesome-Journal-Skills`](https://github.com/brycewang-stanford/Awesome-Journal-Skills) → `TACAS-Skills/skills/tacas-related-work/SKILL.md`
thedixitjain