This index puts every verification method on a row, classified on the axes from the project's methodology and tagged with the quality dimensions it serves. Each method also gets its own page, on a shared template: an intro, What it catches, Tools, When to use, when not, and Evidence. Methods that are related or easily confused carry a Related section on that page.
How to read the table¶
The columns are three of the axes — input, oracle, guarantee — and the quality dimensions each method serves. Those pages define the values; the table places every method on them.
- A dash (—) means the axis doesn't apply: a proof doesn't run code on chosen inputs, so its input cell reads —.
- A method's listed dimensions are where its evidence (or definitional case) is strongest, not the only ones it can serve.
- Footnotes flag methods that don't fit cleanly on a row.
Types and effects¶
The type checker reads the program text without running it. The family spans four tiers, from mainstream type systems to refinement and dependent types.
| Method | Oracle | Guarantee | Quality dimensions served |
|---|---|---|---|
| Static types | Type, Schema | Exhaustive¹ | Functionality, Maintainability |
| Linear types | Type, Schema | Exhaustive² | Functionality, Security, Maintainability |
| Effect systems | Type, Schema | Mathematical³ | Functionality, Maintainability |
| Refinement and dependent types | Type, Schema | Mathematical⁴ | Functionality |
¹ Exhaustive within what the type system can express. A passing type check proves the absence of one bug class (the one the type forbids); it claims nothing about the bug classes outside the system's expressive reach. Only when sound — most mainstream type systems are unsound at one or more boundaries.
² Exhaustive within what the type system can express. A passing type check proves the absence of one bug class (the one the type forbids); it claims nothing about the bug classes outside the system's expressive reach. Only when sound: most mainstream type systems are unsound at one or more boundaries; see the types overview for the soundness discussion.
³ Mathematical only with proof-assistant discharge; a plain effect system is Exhaustive within what it can express, and only when sound (most mainstream type systems are unsound at one or more boundaries — see the types overview). A passing check proves the absence of one bug class; it claims nothing outside the system's expressive reach.
⁴ Exhaustive within the SMT solver's reach for refinement types; Mathematical when paired with proof-assistant discharge — see theorem proving.
Static analysis¶
Pattern- and dataflow-based analysis also reads the source without running it.
| Method | Oracle | Guarantee | Quality dimensions served |
|---|---|---|---|
| Linters | Invariant | Empirical¹ | Functionality, Maintainability |
| Secret scanning | Threshold | Empirical² | Security |
| Deep static analysis — Dataflow and query analysis | Invariant | Empirical³ | Security, Functionality |
| Deep static analysis — ReDoS | Invariant | Empirical⁴ | Security, Reliability |
| Dead-code detection — Unreachable symbols | Invariant | Empirical⁵ | Maintainability |
| Dead-code detection — Unreachable statements | Invariant | Exhaustive⁶ | Maintainability, Functionality |
| Dead-code detection — Infeasible branches | Invariant, Type | Empirical⁷ | Functionality, Maintainability |
| Dead-code detection — Dead stores | Invariant | Exhaustive⁸ | Maintainability, Functionality |
| Clone detection | Threshold | Empirical⁹ | Maintainability, Security |
| Database migration safety | Invariant | Empirical¹⁰ | Reliability |
¹ Definitionally exhaustive over a fixed rule set, but the rule set is incomplete and tuned for false-positive rate — what the tool reports is closer to a high-confidence empirical signal than a guarantee.
² A credential that matches no rule and scores below the entropy threshold is not caught; live-verification cuts false positives but cannot add recall.
³ The engines deliberately under- or over-approximate for scale and false-positive rate; what they report is a high-confidence signal, not a proof.
⁴ NFA analysis is precise only for the patterns it can model; a linear-time engine removes the class by construction.
⁵ Reachability from declared entry points is exhaustive over the static call/import graph, but unsound in general: reflection, string-keyed lookup, and dynamic import() create edges the graph can't see. Some analyses are sound within a narrower scope (Go's deadcode for dynamic dispatch).
⁶ Sound over a deliberately narrow class: statements that a structural transfer of control (return, throw, break, a diverging call) cuts off. The graph abstracts away which conditions hold, so a statement unreachable only because no input satisfies a guard is a separate finding — the Java specification excludes if (false) on purpose, to keep conditional compilation legal.
⁷ Undecidable in general: each engine settles a subset (bounded paths, a widened abstract domain, a computed type) and stays silent on the rest, so an absence of findings is not an absence of infeasible branches. The exception is match-arm usefulness, which is decidable for the pattern language — the reason unreachable_patterns is a warning rather than a hint.
⁸ Decided only for the definitions the analysis tracks — locals it can see whole. A store through a pointer or reference, into a field, or into a variable that escapes the procedure falls outside the class, and tools trade recall for precision by suppressing compiler-generated and idiomatic patterns.
⁹ Exhaustive over the chosen code representation (tokens, AST, embeddings) for a fixed similarity threshold, but precision and recall both move with that threshold. Type-1/2/3 detection is mature; semantic (Type-4) recall is contested and its benchmarks oversell it.
¹⁰ The rules encode known-dangerous operations for a given engine and version; a pattern the rule set does not model is not caught.
Tests — executed against the program¶
These methods construct a scenario (inputs, or injected faults) and check the result. Input, oracle, and guarantee are properties of the test design, whether the scenario runs against a fixture or a production-like system (chaos engineering).
| Method | Input | Oracle | Guarantee | Quality dimensions served |
|---|---|---|---|---|
| Example tests | Fixed | Any | Empirical | Functionality, Maintainability |
| Snapshot and approval testing — value-snapshot | Fixed | Snapshot¹ | Empirical | Functionality, Maintainability |
| Snapshot and approval testing — visual-snapshot | Fixed | Snapshot² | Empirical | Functionality, Maintainability |
| Snapshot and approval testing — recorded-interaction | Fixed | Snapshot³ | Empirical | Functionality, Maintainability |
| Property-based testing — property | Random | Invariant | Empirical | Functionality, Reliability |
| Property-based testing — metamorphic | Random | Metamorphic | Empirical | Functionality |
| Property-based testing — bounded-exhaustive | Exhaustive | Invariant | Exhaustive⁴ | Functionality, Reliability |
| Combinatorial and pairwise testing | Exhaustive | Any | Exhaustive⁵ | Functionality, Reliability |
| Fuzzing | Feedback | Errors, Predicate | Empirical | Security, Functionality, Reliability |
| Automated test generation — search-based | Feedback | Errors | Heuristic⁶ | Functionality, Reliability |
| Automated test generation — feedback-directed random | Random | Errors | Heuristic⁷ | Functionality, Reliability |
| Differential testing | Any | Differential | Empirical | Functionality |
| Metamorphic testing | Any | Metamorphic | Empirical | Functionality |
| Statistical and sampling testing | Random | Statistical | Empirical | Functionality, Reliability |
| Deterministic simulation testing | Random | Invariant | Empirical | Reliability, Functionality |
| Chaos engineering | Random | Aggregate, Invariant | Empirical | Reliability |
| Fault injection | Random | Invariant | Empirical | Reliability |
¹ What is pinned is the serialization, not the value: a change of formatter or custom serializer fails every snapshot at once.
² Equality up to a comparator: the check passes while the difference stays under a tolerance, so it is approximate equality against the approved image rather than byte identity.
³ The recording is the oracle only for the side under check, and a fixture for the other; how strictly the request is matched decides how much of an oracle is left.
⁴ Exhaustive only up to the size / depth bound; beyond it nothing is claimed.
⁵ Exhaustive only over t-way interactions for the chosen t and the chosen per-parameter values; faults that need more than t interacting parameters, or values outside the modeled set, are not covered.
⁶ The generated oracle asserts current behavior, bugs included; high coverage is the objective, not evidence of correctness.
⁷ Same regression-oracle limitation: the captured assertions encode present behavior, not a specification.
Runtime / production¶
These methods observe the live or production system as it runs rather than constructing a scenario. They take the system's behavior as given and report on it, so their guarantee is Heuristic or Empirical.
| Method | Input | Oracle | Guarantee | Quality dimensions served |
|---|---|---|---|---|
| Contracts and runtime assertions | Any | Invariant | Empirical | Functionality |
| Schema and boundary validation | Live | Schema | Empirical | Functionality, Security |
| Monitoring and observability — slo-sli | Live | Aggregate | Heuristic | Reliability, Performance |
| Monitoring and observability — health-checks | Live | Invariant | Heuristic | Reliability |
| Monitoring and observability — error-telemetry | Live | Errors | Heuristic | Reliability |
| Monitoring and observability — field-telemetry | Live | Aggregate | Heuristic | Reliability, Performance |
| Parallel run | Live | Differential | Empirical | Functionality, Maintainability |
| Change-point detection | Fixed | Statistical | Empirical | Maintainability |
Formal methods¶
These methods reason mathematically over a specification or program — a family of techniques rather than a single method. The family overview at formal methods explains how to pick a tier; the sub-pages give the recipe per technique.
| Method | Input | Oracle | Guarantee | Quality dimensions served |
|---|---|---|---|---|
| Model checking | Exhaustive | Formal | Exhaustive | Reliability, Functionality |
| Bounded model checking | Solver | Predicate | Exhaustive¹ | Functionality, Reliability |
| Systematic concurrency testing — Systematic exploration | Exhaustive | Invariant | Exhaustive | Reliability, Functionality |
| Systematic concurrency testing — Randomized scheduling | Random | Invariant | Empirical | Reliability, Functionality |
| Probabilistic model checking — sampling | Random | Statistical | Empirical | Reliability, Performance |
| Probabilistic model checking — exact | Exhaustive | Exact | Exhaustive² | Reliability, Performance |
| Theorem proving | — | Formal | Mathematical | Functionality, Security |
| Symbolic execution — whitebox | Solver | Errors | Exhaustive³ | Functionality, Security |
| Symbolic execution — concolic | Feedback | Errors | Empirical | Functionality, Security |
| Abstract interpretation | — | Invariant | Exhaustive⁴ | Functionality, Reliability, Security |
| Termination analysis | — | Formal | Exhaustive⁵ | Functionality, Reliability |
| WCET analysis | — | Threshold | Exhaustive⁶ | Performance |
| Equivalence checking — complete | Solver | Differential⁷ | Mathematical⁸ | Functionality |
| Equivalence checking — bounded | Solver | Differential | Exhaustive⁹ | Functionality |
| Decision tables — lightweight tier | Fixed | Authored | Exhaustive | Functionality |
| Exhaustive coverage (MC/DC, MCC) — lightweight tier | Fixed | Authored | Exhaustive¹⁰ | Functionality |
| State machines — lightweight tier | —¹¹ | Formal, Invariant | Exhaustive¹² | Functionality |
| Executable specifications — lightweight tier | Any | Differential | Empirical¹³ | Functionality |
¹ Exhaustive only to the configured unwinding depth; executions deeper than k are not checked.
² Exhaustive over the model's reachable states; like all model checking it verifies the model, not the implementation.
³ Exhaustive over the paths the symbolic engine can explore, not over the full input space. Path explosion is the operative cost.
⁴ Sound by over-approximation: no false negatives within the abstraction, but spurious alarms (false positives) are expected, and it proves the absence of a fixed error class — not full functional correctness, and only modulo the analyzer's modeling assumptions.
⁵ Sound but inherently incomplete (the halting problem): a proof of termination holds for every execution, but for any analyzer there are terminating programs it cannot prove terminate. It proves only termination, not what the program computes.
⁶ Sound only relative to the hardware timing model: an unmodeled cache, pipeline, or contention effect breaks the guarantee or inflates the bound. Measurement-based WCET (run on the target, take the max plus a margin) is the practical alternative but is not sound — it can miss the true worst case.
⁷ The reference is usually a second implementation or representation (translation validation: compiled output vs source; hardware: RTL vs netlist). When it is a written specification the oracle shades into Reference.
⁸ Mathematical only when the check is complete — a decidable theory or finite state, as in hardware logic-equivalence checking. Unbounded software is handled by the bounded instance.
⁹ Exhaustive only to the modeled depth (alive2's loop unrolling, CBMC's unwinding bound); equivalence beyond the bound is not established.
¹⁰ Exhaustive only inside a finite, deterministic Boolean envelope and only with a sound oracle on each case — the criterion proves every combination was run, never that each produced the right answer.
¹¹ The chart as a model is read or model-checked. Using it to drive an implementation is model-based / stateful PBT — see property-based testing; the model is then an input shape, not the oracle.
¹² Exhaustive over the transition graph when the chart is compiler- or model-checked (illegal and forgotten transitions are rejected); Empirical when only exercised by tests; Heuristic when merely drawn and read. Logic inside a transition, and concurrency interleavings, stay out of scope — lift to model checking.
¹³ Heuristic where the spec runs once.
Domain-specific verification¶
These methods aim at a specific quality concern rather than general correctness: security, performance, the supply chain.
Security¶
Methods that probe for exploitable weakness: adversarial inputs, tainted data flows, and dependency risk.
| Method | Input | Oracle | Guarantee | Quality dimensions served |
|---|---|---|---|---|
| Threat modeling | — | — | — | Security |
| Penetration testing — manual-exploitation | — | Errors | Heuristic | Security |
| Penetration testing — exploitability-triage | — | Human | Heuristic | Security |
| Taint analysis — static | — | Invariant | Empirical¹ | Security |
| Taint analysis — dynamic | Live | Invariant | Empirical | Security |
| Supply-chain hygiene | — | Membership | Empirical | Security, Maintainability |
| Agent security testing — injection-corpus | Random | Membership | Empirical² | Security |
| Agent security testing — adaptive-attack | — | Errors | Heuristic | Security |
| Agent security testing — tool-surface-scan | — | Membership | Heuristic | Security |
Safety¶
Methods for systems where a failure causes physical harm, judged against a safety envelope rather than a functional spec.
| Method | Input | Oracle | Guarantee | Quality dimensions served |
|---|---|---|---|---|
| Safety analysis | — | — | — | Functionality |
| Testing autonomous systems | — | — | — | Functionality, Reliability |
| Temporal-logic falsification | Feedback | Formal | Empirical³ | Functionality, Reliability, Performance |
Performance¶
Methods that measure time, throughput, and resource use rather than functional correctness.
| Method | Input | Oracle | Guarantee | Quality dimensions served |
|---|---|---|---|---|
| Algorithmic complexity testing | Feedback | Threshold | Empirical | Performance, Security |
| Load and stress testing | Random | Aggregate | Empirical | Performance, Reliability |
| Profiling | Fixed | Aggregate | Heuristic | Performance |
| Microbenchmarking | Fixed | Statistical | Heuristic | Performance |
Other¶
| Method | Input | Oracle | Guarantee | Quality dimensions served |
|---|---|---|---|---|
| Testing ML systems | — | — | — | Functionality, Reliability, Security |
| Testing GUI and mobile apps | Random, Feedback | Errors | Empirical | Reliability, Functionality, Performance |
¹ A sound information-flow analysis proves non-interference, but the deployed SAST engines (CodeQL, Semgrep, Zoncolan) deliberately under- or over-approximate for scale and false-positive rate, and most do not track implicit (control-flow) flows — what they report is a high-confidence signal, not a proof.
² The rate is a lower bound. A corpus measures resistance to the attacks written into it, and an attacker who reads the corpus writes the next one.
³ Sound for bugs, not complete: no falsifying input found does not mean none exists. For a guarantee, pair with reachability analysis or model checking.
Methods on the test suite itself¶
This family takes the suite as its object, not the code. The test suite as an object is the overview: it glosses how effective the suite is (measuring effectiveness, mutation testing), what it costs to run (regression-suite management: prioritization, selection, minimization), and its flakiness and maintainability, linking each to its page. All of it measures or reorganizes the suite rather than judging a run, so it sits off the code-verification axes.
| Method | Quality dimensions served |
|---|---|
| Coverage | Maintainability |
| Mutation testing | Maintainability |
| Test case prioritization | Maintainability |
| Regression test selection | Maintainability |
| Test suite minimization | Maintainability |
Process methods¶
These methods judge the code, design, or process rather than a run's output, so they sit off every axis. The table records only the quality dimensions they serve.
| Method | Quality dimensions served |
|---|---|
| Code review | Maintainability, Functionality |
| Architecture decision records | Maintainability |
| Refactoring practice | Maintainability |
| Git-history hotspots | Maintainability |
| Requirements quality checking | Functionality |
| Checklists | Reliability, Security, Functionality |
What the table is for¶
Three uses:
- A row. A method's row names the kind of uncertainty it reduces (the axes) and the quality dimensions it serves, which together decide whether it fits a project's bug-risk profile.
- A column. The dimensions column shows which methods serve a given quality dimension. The corresponding dimension page in Quality dimensions curates the order to adopt them in.
- The gaps. A team running only Fixed in the Input column has covered one cell. A team running Empirical across every row has none of the Exhaustive or Mathematical guarantees. The blind spots become visible.
The table is a thinking device, not a ranking: the recommendations live in the per-method Evidence sections and on the choosing methods page.
Referenced by¶
- The axes · The axes
- Recipes · Recipes
- How AI fits into software quality · AI
- Conventional · Conventional
- Testing folklore · Conventional
- About this project and how it is checked · Overview
- Choosing methods · Overview
- Software Quality · Overview