# Methods — index and classification

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.

<!-- viz: frontier -->

## How to read the table

The columns are three of the [axes](https://quality.stereobooster.com/axes.md) —
[input](https://quality.stereobooster.com/input.md), [oracle](https://quality.stereobooster.com/oracle.md),
[guarantee](https://quality.stereobooster.com/guarantee.md) — and the [quality
dimensions](https://quality.stereobooster.com/quality-dimensions.md) 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](https://quality.stereobooster.com/static-types.md) | Type, Schema | Exhaustive¹ | Functionality, Maintainability |
| [Linear types](https://quality.stereobooster.com/linear-types.md) | Type, Schema | Exhaustive² | Functionality, Security, Maintainability |
| [Effect systems](https://quality.stereobooster.com/effect-systems.md) | Type, Schema | Mathematical³ | Functionality, Maintainability |
| [Refinement and dependent types](https://quality.stereobooster.com/refinement-and-dependent-types.md) | 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](https://quality.stereobooster.com/types.md) 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](https://quality.stereobooster.com/types.md)). 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](https://quality.stereobooster.com/theorem-proving.md).*

## Static analysis

Pattern- and dataflow-based analysis also reads the source without
running it.

| Method | Oracle | Guarantee | Quality dimensions served |
| --- | --- | --- | --- |
| [Linters](https://quality.stereobooster.com/linters.md) | Invariant | Empirical¹ | Functionality, Maintainability |
| [Secret scanning](https://quality.stereobooster.com/secret-scanning.md) | Threshold | Empirical² | Security |
| [Deep static analysis](https://quality.stereobooster.com/deep-static-analysis.md) — [Dataflow and query analysis](https://quality.stereobooster.com/deep-static-analysis.md#dataflow-and-query-analysis) | Invariant | Empirical³ | Security, Functionality |
| [Deep static analysis](https://quality.stereobooster.com/deep-static-analysis.md) — [ReDoS](https://quality.stereobooster.com/deep-static-analysis.md#redos) | Invariant | Empirical⁴ | Security, Reliability |
| [Dead-code detection](https://quality.stereobooster.com/dead-code-detection.md) — [Unreachable symbols](https://quality.stereobooster.com/dead-code-detection.md#unreachable-symbols) | Invariant | Empirical⁵ | Maintainability |
| [Dead-code detection](https://quality.stereobooster.com/dead-code-detection.md) — [Unreachable statements](https://quality.stereobooster.com/dead-code-detection.md#unreachable-statements) | Invariant | Exhaustive⁶ | Maintainability, Functionality |
| [Dead-code detection](https://quality.stereobooster.com/dead-code-detection.md) — [Infeasible branches](https://quality.stereobooster.com/dead-code-detection.md#infeasible-branches) | Invariant, Type | Empirical⁷ | Functionality, Maintainability |
| [Dead-code detection](https://quality.stereobooster.com/dead-code-detection.md) — [Dead stores](https://quality.stereobooster.com/dead-code-detection.md#dead-stores) | Invariant | Exhaustive⁸ | Maintainability, Functionality |
| [Clone detection](https://quality.stereobooster.com/clone-detection.md) | Threshold | Empirical⁹ | Maintainability, Security |
| [Database migration safety](https://quality.stereobooster.com/migration-safety.md) | 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](https://quality.stereobooster.com/example-tests.md) | Fixed | Any | Empirical | Functionality, Maintainability |
| [Snapshot and approval testing](https://quality.stereobooster.com/snapshot-testing.md) — [value-snapshot](https://quality.stereobooster.com/snapshot-testing.md#value-snapshot) | Fixed | Snapshot¹ | Empirical | Functionality, Maintainability |
| [Snapshot and approval testing](https://quality.stereobooster.com/snapshot-testing.md) — [visual-snapshot](https://quality.stereobooster.com/snapshot-testing.md#visual-snapshot) | Fixed | Snapshot² | Empirical | Functionality, Maintainability |
| [Snapshot and approval testing](https://quality.stereobooster.com/snapshot-testing.md) — [recorded-interaction](https://quality.stereobooster.com/snapshot-testing.md#recorded-interaction) | Fixed | Snapshot³ | Empirical | Functionality, Maintainability |
| [Property-based testing](https://quality.stereobooster.com/property-based-testing.md) — property | Random | Invariant | Empirical | Functionality, Reliability |
| [Property-based testing](https://quality.stereobooster.com/property-based-testing.md) — metamorphic | Random | Metamorphic | Empirical | Functionality |
| [Property-based testing](https://quality.stereobooster.com/property-based-testing.md) — bounded-exhaustive | Exhaustive | Invariant | Exhaustive⁴ | Functionality, Reliability |
| [Combinatorial and pairwise testing](https://quality.stereobooster.com/combinatorial-testing.md) | Exhaustive | Any | Exhaustive⁵ | Functionality, Reliability |
| [Fuzzing](https://quality.stereobooster.com/fuzzing.md) | Feedback | Errors, Predicate | Empirical | Security, Functionality, Reliability |
| [Automated test generation](https://quality.stereobooster.com/automated-test-generation.md) — search-based | Feedback | Errors | Heuristic⁶ | Functionality, Reliability |
| [Automated test generation](https://quality.stereobooster.com/automated-test-generation.md) — feedback-directed random | Random | Errors | Heuristic⁷ | Functionality, Reliability |
| [Differential testing](https://quality.stereobooster.com/differential-testing.md) | Any | Differential | Empirical | Functionality |
| [Metamorphic testing](https://quality.stereobooster.com/metamorphic-testing.md) | Any | Metamorphic | Empirical | Functionality |
| [Statistical and sampling testing](https://quality.stereobooster.com/statistical-testing.md) | Random | Statistical | Empirical | Functionality, Reliability |
| [Deterministic simulation testing](https://quality.stereobooster.com/deterministic-simulation-testing.md) | Random | Invariant | Empirical | Reliability, Functionality |
| [Chaos engineering](https://quality.stereobooster.com/chaos-engineering.md) | Random | Aggregate, Invariant | Empirical | Reliability |
| [Fault injection](https://quality.stereobooster.com/fault-injection.md) | 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](https://quality.stereobooster.com/contracts-and-runtime-assertions.md) | Any | Invariant | Empirical | Functionality |
| [Schema and boundary validation](https://quality.stereobooster.com/schema-and-boundary-validation.md) | Live | Schema | Empirical | Functionality, Security |
| [Monitoring and observability](https://quality.stereobooster.com/monitoring-and-observability.md) — slo-sli | Live | Aggregate | Heuristic | Reliability, Performance |
| [Monitoring and observability](https://quality.stereobooster.com/monitoring-and-observability.md) — health-checks | Live | Invariant | Heuristic | Reliability |
| [Monitoring and observability](https://quality.stereobooster.com/monitoring-and-observability.md) — error-telemetry | Live | Errors | Heuristic | Reliability |
| [Monitoring and observability](https://quality.stereobooster.com/monitoring-and-observability.md) — [field-telemetry](https://quality.stereobooster.com/monitoring-and-observability.md#field-telemetry) | Live | Aggregate | Heuristic | Reliability, Performance |
| [Parallel run](https://quality.stereobooster.com/parallel-run.md) | Live | Differential | Empirical | Functionality, Maintainability |
| [Change-point detection](https://quality.stereobooster.com/change-point-detection.md) | 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](https://quality.stereobooster.com/formal.md) explains how to pick a tier; the
sub-pages give the recipe per technique.

| Method | Input | Oracle | Guarantee | Quality dimensions served |
| --- | --- | --- | --- | --- |
| [Model checking](https://quality.stereobooster.com/model-checking.md) | Exhaustive | Formal | Exhaustive | Reliability, Functionality |
| [Bounded model checking](https://quality.stereobooster.com/bounded-model-checking.md) | Solver | Predicate | Exhaustive¹ | Functionality, Reliability |
| [Systematic concurrency testing](https://quality.stereobooster.com/systematic-concurrency-testing.md) — [Systematic exploration](https://quality.stereobooster.com/systematic-concurrency-testing.md#systematic-exploration) | Exhaustive | Invariant | Exhaustive | Reliability, Functionality |
| [Systematic concurrency testing](https://quality.stereobooster.com/systematic-concurrency-testing.md) — [Randomized scheduling](https://quality.stereobooster.com/systematic-concurrency-testing.md#randomized-scheduling) | Random | Invariant | Empirical | Reliability, Functionality |
| [Probabilistic model checking](https://quality.stereobooster.com/probabilistic-model-checking.md) — sampling | Random | Statistical | Empirical | Reliability, Performance |
| [Probabilistic model checking](https://quality.stereobooster.com/probabilistic-model-checking.md) — exact | Exhaustive | Exact | Exhaustive² | Reliability, Performance |
| [Theorem proving](https://quality.stereobooster.com/theorem-proving.md) | — | Formal | Mathematical | Functionality, Security |
| [Symbolic execution](https://quality.stereobooster.com/symbolic-execution.md) — whitebox | Solver | Errors | Exhaustive³ | Functionality, Security |
| [Symbolic execution](https://quality.stereobooster.com/symbolic-execution.md) — concolic | Feedback | Errors | Empirical | Functionality, Security |
| [Abstract interpretation](https://quality.stereobooster.com/abstract-interpretation.md) | — | Invariant | Exhaustive⁴ | Functionality, Reliability, Security |
| [Termination analysis](https://quality.stereobooster.com/termination-analysis.md) | — | Formal | Exhaustive⁵ | Functionality, Reliability |
| [WCET analysis](https://quality.stereobooster.com/wcet-analysis.md) | — | Threshold | Exhaustive⁶ | Performance |
| [Equivalence checking](https://quality.stereobooster.com/equivalence-checking.md) — complete | Solver | Differential⁷ | Mathematical⁸ | Functionality |
| [Equivalence checking](https://quality.stereobooster.com/equivalence-checking.md) — bounded | Solver | Differential | Exhaustive⁹ | Functionality |
| [Decision tables](https://quality.stereobooster.com/decision-tables.md) — *lightweight tier* | Fixed | Authored | Exhaustive | Functionality |
| [Exhaustive coverage (MC/DC, MCC)](https://quality.stereobooster.com/exhaustive-coverage.md) — *lightweight tier* | Fixed | Authored | Exhaustive¹⁰ | Functionality |
| [State machines](https://quality.stereobooster.com/state-machines.md) — *lightweight tier* | —¹¹ | Formal, Invariant | Exhaustive¹² | Functionality |
| [Executable specifications](https://quality.stereobooster.com/executable-specifications.md) — *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](https://quality.stereobooster.com/property-based-testing.md); 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](https://quality.stereobooster.com/model-checking.md).*

¹³ *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](https://quality.stereobooster.com/threat-modeling.md) | — | — | — | Security |
| [Penetration testing](https://quality.stereobooster.com/penetration-testing.md) — manual-exploitation | — | Errors | Heuristic | Security |
| [Penetration testing](https://quality.stereobooster.com/penetration-testing.md) — exploitability-triage | — | Human | Heuristic | Security |
| [Taint analysis](https://quality.stereobooster.com/taint-analysis.md) — static | — | Invariant | Empirical¹ | Security |
| [Taint analysis](https://quality.stereobooster.com/taint-analysis.md) — dynamic | Live | Invariant | Empirical | Security |
| [Supply-chain hygiene](https://quality.stereobooster.com/supply-chain-hygiene.md) | — | Membership | Empirical | Security, Maintainability |
| [Agent security testing](https://quality.stereobooster.com/agent-security-testing.md) — [injection-corpus](https://quality.stereobooster.com/agent-security-testing.md#injection-corpus) | Random | Membership | Empirical² | Security |
| [Agent security testing](https://quality.stereobooster.com/agent-security-testing.md) — [adaptive-attack](https://quality.stereobooster.com/agent-security-testing.md#adaptive-attack) | — | Errors | Heuristic | Security |
| [Agent security testing](https://quality.stereobooster.com/agent-security-testing.md) — [tool-surface-scan](https://quality.stereobooster.com/agent-security-testing.md#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](https://quality.stereobooster.com/safety-analysis.md) | — | — | — | Functionality |
| [Testing autonomous systems](https://quality.stereobooster.com/testing-autonomous-systems.md) | — | — | — | Functionality, Reliability |
| [Temporal-logic falsification](https://quality.stereobooster.com/temporal-logic-falsification.md) | 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](https://quality.stereobooster.com/algorithmic-complexity.md) | Feedback | Threshold | Empirical | Performance, Security |
| [Load and stress testing](https://quality.stereobooster.com/load-and-stress-testing.md) | Random | Aggregate | Empirical | Performance, Reliability |
| [Profiling](https://quality.stereobooster.com/profiling.md) | Fixed | Aggregate | Heuristic | Performance |
| [Microbenchmarking](https://quality.stereobooster.com/microbenchmarking.md) | Fixed | Statistical | Heuristic | Performance |

### Other

| Method | Input | Oracle | Guarantee | Quality dimensions served |
| --- | --- | --- | --- | --- |
| [Testing ML systems](https://quality.stereobooster.com/testing-ml-systems.md) | — | — | — | Functionality, Reliability, Security |
| [Testing GUI and mobile apps](https://quality.stereobooster.com/testing-gui-and-mobile-apps.md) | 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](https://quality.stereobooster.com/test-suite.md) 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](https://quality.stereobooster.com/coverage.md) | Maintainability |
| [Mutation testing](https://quality.stereobooster.com/mutation-testing.md) | Maintainability |
| [Test case prioritization](https://quality.stereobooster.com/test-case-prioritization.md) | Maintainability |
| [Regression test selection](https://quality.stereobooster.com/regression-test-selection.md) | Maintainability |
| [Test suite minimization](https://quality.stereobooster.com/test-suite-minimization.md) | 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](https://quality.stereobooster.com/code-review.md) | Maintainability, Functionality |
| [Architecture decision records](https://quality.stereobooster.com/adrs.md) | Maintainability |
| [Refactoring practice](https://quality.stereobooster.com/refactoring-practice.md) | Maintainability |
| [Git-history hotspots](https://quality.stereobooster.com/git-hotspots.md) | Maintainability |
| [Requirements quality checking](https://quality.stereobooster.com/requirements-quality-checking.md) | Functionality |
| [Checklists](https://quality.stereobooster.com/checklists.md) | Reliability, Security, Functionality |

## What the table is for

Three uses:

1. **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.
2. **A column.** The dimensions column shows which methods serve a
   given quality dimension. The corresponding dimension page in
   [Quality dimensions](https://quality.stereobooster.com/quality-dimensions.md) curates the order to adopt them in.
3. **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](https://quality.stereobooster.com/choosing.md) page.

## Referenced by

- [The axes](https://quality.stereobooster.com/axes.md) · The axes
- [Recipes](https://quality.stereobooster.com/recipes.md) · Recipes
- [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI
- [Conventional](https://quality.stereobooster.com/conventional.md) · Conventional
- [Testing folklore](https://quality.stereobooster.com/testing-folklore.md) · Conventional
- [About this project and how it is checked](https://quality.stereobooster.com/about.md) · Overview
- [Choosing methods](https://quality.stereobooster.com/choosing.md) · Overview
- [Software Quality](https://quality.stereobooster.com/index.md) · Overview

## Acronyms

- AST — abstract syntax tree
- MC/DC — modified condition/decision coverage
- MCC — multiple-condition coverage
- PBT — property-based testing
- RTL — register-transfer level
- SAST — static application security testing
- SMT — satisfiability modulo theories
- WCET — worst-case execution time