CAV Topic Selection
Decide the venue and the category before drafting. CAV — the International Conference on Computer
Aided Verification — is the flagship venue for computer-aided formal analysis of hardware and
software systems: model checking, SMT and theorem proving, program analysis and synthesis, and
their tools. Its papers are Springer LNCS chapters read by verification researchers, so reviewers
reward a durable verification contribution with a stated guarantee, not a systems demo or an ML
result with a verification label attached.
Two decisions, not one
At CAV you choose both a venue (CAV vs. its siblings) and a category (Regular vs. Tool vs.
Application vs. Industrial). Get the venue right first, then the category — a strong tool filed as a
Regular Paper, or a technique squeezed into a 10-page tool paper, wastes the fit.
Sibling-venue routing table
| Signal in your project |
Better home |
Why |
| A general verification technique/algorithm with a soundness/completeness result, mature enough for the flagship |
CAV |
Flagship scope; the Regular-Paper archetype |
| Emphasis on tools, algorithms, and their construction/analysis, or you want the ETAPS calendar |
TACAS |
Tools and Algorithms for the Construction and Analysis of Systems; overlaps heavily but is a distinct venue |
| Hardware-oriented or applied model checking, or a formal-methods-in-design focus |
FMCAD |
Formal Methods in Computer-Aided Design |
| Verification, model checking, and abstract interpretation with a foundations flavor, often earlier-stage |
VMCAI |
Verification, Model Checking, and Abstract Interpretation |
| Automated/interactive theorem proving or logic-focused |
IJCAR / LPAR / ITP / CADE |
Reasoning and proof communities |
| The core is a programming-language semantics, type system, or PL analysis |
POPL / PLDI / OOPSLA |
PL venues; verification is a means, not the contribution |
| The study is too long or too deep for the page limit |
FMSD / JAR / TOCL / STTT |
Journals with no conference page ceiling |
CAV and TACAS overlap the most; the honest tie-breakers are the calendar (CAV is annual in
mid-year, often under FLoC or standalone; TACAS runs at ETAPS in spring) and community pull for
your subarea. A strong paper is publishable at either — route to the nearer honest fit.
Contribution shapes CAV rewards
- Technique / algorithm with a guarantee — a new decision procedure, model-checking algorithm,
abstraction, invariant-synthesis method, or proof technique, with a stated soundness/completeness
property and evidence it scales past prior methods (the CEGAR / interpolation lineage).
- Tool paper — a usable, downloadable verification tool (solver, model checker, prover, analyzer)
evaluated on standard benchmarks, with the engineering foregrounded (the CVC4 / Marabou lineage).
- New application domain — bringing a hard real problem into verification's scope with a real
technique (the neural-network-verification lineage).
- Application / case study / industrial experience — applying verification to a concrete system
and reporting what worked, what did not, and what generalizes.
The re-label and swap tests
Two quick tests sharpen a borderline verdict:
- Guarantee test: does your contribution come with a formal property (soundness, completeness,
an equisatisfiability or refinement claim)? If the "result" is only a benchmark score with no
guarantee, it may be a tool note (TACAS) or a heuristic paper, not a CAV Regular Paper.
- Re-label test: could this paper be submitted to FMCAD or VMCAI unchanged and read as native
there? If its heart is hardware-design methodology or early-stage abstract interpretation, route
accordingly; CAV rewards the general, flagship framing.
Category-selection cues (once CAV is chosen)
[Regular] a technique/algorithm + proof + benchmark evaluation -> 18 pages, anonymized
[Short Tool] a downloadable tool; the contribution is the usable system -> 10 pages, NOT anonymized
[Short App] verification applied to a specific problem, technique-light -> 10 pages, anonymized
[Industrial] a real/industrial deployment experience or case study -> 10 pages, NOT anonymized
If you have both a technique and a tool, the usual move is a Regular Paper that describes the
technique with the tool as its evaluation vehicle — reserve the Tool Paper for when the system
itself is the contribution.
Cheap reconnaissance before committing
[Scope] scan the last two CAV programs (dblp, i-cav.org) for your subarea
-> 3+ recent papers = a reviewer pool exists; 0 = opening or mismatch
[Benchmarks] is there a standard benchmark set (SV-COMP, SMT-COMP, HWMCC, VNN-COMP) reviewers expect?
-> yes and you did not use it => reframe or add it before submitting
[Calendar] compare the next CAV deadline with TACAS/FMCAD/VMCAI dates -> route to the nearest
honest fit rather than idling a cycle
Decision procedure
[Audience] who acts differently if the claim holds? -> verification-tool builders/users/theorists?
[Claim type] technique-with-guarantee / tool / application / industrial experience
[CAV vs sibling] both fit? -> choose by calendar, community pull, and hardware/PL/logic tilt
[Category] technique+proof -> Regular; usable system -> Tool; applied -> Application/Industrial
[Verdict] CAV <category> / sibling venue / 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 CAV, continue with cav-workflow for the calendar and cav-writing-style for
the paper shape.
Source: brycewang-stanford/Awesome-Journal-Skills → CAV-Skills/skills/cav-topic-selection/SKILL.md
1---2name: cav-topic-selection3description: Use when deciding whether a formal-methods project belongs at CAV (Computer Aided Verification) or should be routed to TACAS, FMCAD, VMCAI, LPAR/IJCAR, POPL/PLDI/OOPSLA, or a journal (FMSD/JAR/TOCL), and when choosing the right CAV category — Regular, Short Tool, Short Application, or Industrial Experience & Case Study.4---567# CAV Topic Selection89Decide the venue and the category before drafting. CAV — the International Conference on Computer10Aided Verification — is the **flagship** venue for computer-aided formal analysis of hardware and11software systems: model checking, SMT and theorem proving, program analysis and synthesis, and12their tools. Its papers are Springer LNCS chapters read by verification researchers, so reviewers13reward a **durable verification contribution with a stated guarantee**, not a systems demo or an ML14result with a verification label attached.1516## Two decisions, not one1718At CAV you choose both a **venue** (CAV vs. its siblings) and a **category** (Regular vs. Tool vs.19Application vs. Industrial). Get the venue right first, then the category — a strong tool filed as a20Regular Paper, or a technique squeezed into a 10-page tool paper, wastes the fit.2122## Sibling-venue routing table2324| Signal in your project | Better home | Why |25|---|---|---|26| A general verification technique/algorithm with a soundness/completeness result, mature enough for the flagship | **CAV** | Flagship scope; the Regular-Paper archetype |27| Emphasis on tools, algorithms, and their construction/analysis, or you want the ETAPS calendar | **TACAS** | Tools and Algorithms for the Construction and Analysis of Systems; overlaps heavily but is a distinct venue |28| Hardware-oriented or applied model checking, or a formal-methods-in-design focus | **FMCAD** | Formal Methods in Computer-Aided Design |29| Verification, model checking, and abstract interpretation with a foundations flavor, often earlier-stage | **VMCAI** | Verification, Model Checking, and Abstract Interpretation |30| Automated/interactive theorem proving or logic-focused | **IJCAR / LPAR / ITP / CADE** | Reasoning and proof communities |31| The core is a programming-language semantics, type system, or PL analysis | **POPL / PLDI / OOPSLA** | PL venues; verification is a means, not the contribution |32| The study is too long or too deep for the page limit | **FMSD / JAR / TOCL / STTT** | Journals with no conference page ceiling |3334CAV and TACAS overlap the most; the honest tie-breakers are the **calendar** (CAV is annual in35mid-year, often under FLoC or standalone; TACAS runs at ETAPS in spring) and **community pull** for36your subarea. A strong paper is publishable at either — route to the nearer honest fit.3738## Contribution shapes CAV rewards3940- **Technique / algorithm with a guarantee** — a new decision procedure, model-checking algorithm,41 abstraction, invariant-synthesis method, or proof technique, with a stated soundness/completeness42 property and evidence it scales past prior methods (the CEGAR / interpolation lineage).43- **Tool paper** — a usable, downloadable verification tool (solver, model checker, prover, analyzer)44 evaluated on standard benchmarks, with the engineering foregrounded (the CVC4 / Marabou lineage).45- **New application domain** — bringing a hard real problem into verification's scope with a real46 technique (the neural-network-verification lineage).47- **Application / case study / industrial experience** — applying verification to a concrete system48 and reporting what worked, what did not, and what generalizes.4950## The re-label and swap tests5152Two quick tests sharpen a borderline verdict:5354- **Guarantee test:** does your contribution come with a formal property (soundness, completeness,55 an equisatisfiability or refinement claim)? If the "result" is only a benchmark score with no56 guarantee, it may be a tool note (TACAS) or a heuristic paper, not a CAV Regular Paper.57- **Re-label test:** could this paper be submitted to FMCAD or VMCAI unchanged and read as native58 there? If its heart is hardware-design methodology or early-stage abstract interpretation, route59 accordingly; CAV rewards the general, flagship framing.6061## Category-selection cues (once CAV is chosen)6263```text64[Regular] a technique/algorithm + proof + benchmark evaluation -> 18 pages, anonymized65[Short Tool] a downloadable tool; the contribution is the usable system -> 10 pages, NOT anonymized66[Short App] verification applied to a specific problem, technique-light -> 10 pages, anonymized67[Industrial] a real/industrial deployment experience or case study -> 10 pages, NOT anonymized68```6970If you have both a technique and a tool, the usual move is a Regular Paper that describes the71technique with the tool as its evaluation vehicle — reserve the Tool Paper for when the *system72itself* is the contribution.7374## Cheap reconnaissance before committing7576```text77[Scope] scan the last two CAV programs (dblp, i-cav.org) for your subarea78 -> 3+ recent papers = a reviewer pool exists; 0 = opening or mismatch79[Benchmarks] is there a standard benchmark set (SV-COMP, SMT-COMP, HWMCC, VNN-COMP) reviewers expect?80 -> yes and you did not use it => reframe or add it before submitting81[Calendar] compare the next CAV deadline with TACAS/FMCAD/VMCAI dates -> route to the nearest82 honest fit rather than idling a cycle83```8485## Decision procedure8687```text88[Audience] who acts differently if the claim holds? -> verification-tool builders/users/theorists?89[Claim type] technique-with-guarantee / tool / application / industrial experience90[CAV vs sibling] both fit? -> choose by calendar, community pull, and hardware/PL/logic tilt91[Category] technique+proof -> Regular; usable system -> Tool; applied -> Application/Industrial92[Verdict] CAV <category> / sibling venue / journal, with a one-line reason93```9495Run this before the writing skills; a wrong venue or category decision wastes every later step.96When the verdict is CAV, continue with `cav-workflow` for the calendar and `cav-writing-style` for97the paper shape.9899---100101**Source:** [`brycewang-stanford/Awesome-Journal-Skills`](https://github.com/brycewang-stanford/Awesome-Journal-Skills) → `CAV-Skills/skills/cav-topic-selection/SKILL.md`
thedixitjain