# Abstract interpretation Abstract interpretation reasons about every possible run of a program at once, by computing with ranges of values instead of actual ones. Those ranges are an **abstract domain** — intervals, octagons, polyhedra — and the analysis finds a fixpoint that **soundly over-approximates** every state the program can reach on any input. If that over-approximation contains no error state (no integer overflow, no out-of-bounds access, no division by zero), then the program is *provably free* of that error class, over all executions at once. The over-approximation also covers states the program cannot reach, so some of its alarms are **false positives** on code that is safe. The framework was set out by Cousot and Cousot (Cousot and Cousot 1977)[^cousot1977]. ## What it catches - **Whole classes of runtime error, proved absent.** Arithmetic overflow, division by zero, out-of-bounds array and pointer access, null dereference, uninitialized reads: each, over every execution, not a sample. - **Numerical invariants.** Ranges and linear relationships between variables (an index stays within an array's bounds; a counter never exceeds a limit) that hold at a program point on all paths. - **Memory-safety and resource properties.** Null-dereference and resource-leak analyses built on separation-logic abstract domains. What it does **not** establish: full functional correctness; it proves the absence of a *fixed class* of fault, not that the program computes the intended result (that is [theorem proving](https://quality.stereobooster.com/theorem-proving.md)). Its soundness also holds only *within the abstraction and its modeling assumptions*: an analyzer that doesn't model a language feature, or assumes it away, can be unsound at that boundary. ## The precision–cost knob The abstract domain sets both what the analyzer can prove and what it costs. **Intervals** ($x \in [a, b]$) are cheap but cannot relate two variables; **octagons** ($\pm x \pm y \le c$) capture simple relationships; **polyhedra** (arbitrary linear inequalities) are the most precise and the most expensive. A coarser domain is faster but raises more false alarms; a richer one proves more but can blow up on large code. Two further mechanics make the fixpoint tractable: **widening** forces convergence on loops (trading precision for termination), and **narrowing** recovers some of the lost precision afterwards. ## Tools These run the analysis *soundly*: - **Astrée** (commercial) — a sound analyzer for absence-of-runtime-errors, tuned for synchronous control code. - **[Frama-C](https://www.frama-c.com/)** — its Eva plugin is an abstract interpreter for C; part of a broader analysis platform. - **[IKOS](https://github.com/NASA-SW-VnV/ikos)** (NASA) — an LLVM-based engine for proving the absence of runtime errors in C/C++; and **[MOPSA](https://mopsa.lip6.fr/)** (academic) — a modular, sound-by-design platform analyzing C and Python. ## When to use, when not **Use:** - Embedded and safety-critical C/C++ where the *absence* of runtime errors must be demonstrated, not just tested: avionics, automotive, aerospace, under regimes like DO-178C. - Numerical code where the properties of interest are ranges and linear relationships an abstract domain expresses well. **Don't:** - When the false-alarm triage cost outweighs the benefit: on unrestricted code a sound configuration can raise more alarms than a team can work through. - For properties the available abstract domains cannot express; the result is either imprecision (alarms) or unsoundness (if the domain silently drops the property). ## Where it sits among the neighbors - **vs [linters](https://quality.stereobooster.com/linters.md):** same "analyze without running," opposite trade. Linters are Empirical and unsound (tuned against false positives); abstract interpretation is sound (tuned against false negatives). Many real tools sit on a dial between the two: Meta's [Infer](https://fbinfer.com/), though built on separation-logic abstract interpretation, is deliberately tuned against false positives, and in its incorrectness-logic form *under*-approximates to report only real bugs, the dual of the sound analysis here. - **vs [symbolic execution](https://quality.stereobooster.com/symbolic-execution.md):** duals. Symbolic execution *under*-approximates: it reasons about the concrete paths it can reach, precisely. Abstract interpretation *over*-approximates: it covers all executions, soundly, but imprecisely. - **vs [theorem proving](https://quality.stereobooster.com/theorem-proving.md):** abstract interpretation is automatic but proves a fixed property class; theorem proving is manual but can prove anything. The cost and the generality move together. ## Evidence - **Astrée on Airbus flight control.** Astrée proved the absence of runtime errors in the primary flight-control software of the A340 and A380 (large, synchronous control code), with **zero false alarms** after the domains were tuned to that code style (Blanchet et al. 2003)[^blanchet2003]. The zero-false-alarm precision is specific to that restricted style of generated code, not arbitrary C. ## Classification - **Quality dimensions:** Functionality, Reliability, Security. - **Area:** Safety-critical and embedded C/C++ (avionics, automotive, aerospace); proving the absence of whole classes of runtime error — overflow, division by zero, out-of-bounds, null dereference — over every execution; numerical and memory-safety properties at scale. - **Guarantee:** Exhaustive — a sound over-approximation: if the analyzer reports no error of the targeted class, none can occur on any run. ## Referenced by - [Dead-code detection](https://quality.stereobooster.com/dead-code-detection.md) · Methods - [Formal methods](https://quality.stereobooster.com/formal.md) · Methods - [Temporal-logic falsification](https://quality.stereobooster.com/temporal-logic-falsification.md) · Methods - [Termination analysis](https://quality.stereobooster.com/termination-analysis.md) · Methods - [Testing machine-learning systems](https://quality.stereobooster.com/testing-ml-systems.md) · Methods - [Verifying memory safety](https://quality.stereobooster.com/memory.md) · Methods - [Verifying numerical code](https://quality.stereobooster.com/numbers.md) · Methods - [Verifying safety-critical systems](https://quality.stereobooster.com/safety.md) · Methods - [Worst-case execution-time analysis](https://quality.stereobooster.com/wcet-analysis.md) · Methods - [Conventional terminology](https://quality.stereobooster.com/terminology.md) · Conventional - [Glossary](https://quality.stereobooster.com/glossary.md) · Overview ## References [^cousot1977]: Cousot, Patrick, and Radhia Cousot. 1977. "[Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints](https://cs.nyu.edu/~pcousot/publications.www/CSV-2023-cousot.pdf)." *Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '77)*, 238–52. . [^blanchet2003]: Blanchet, Bruno, Patrick Cousot, Radhia Cousot, et al. 2003. "[A Static Analyzer for Large Safety-Critical Software](https://arxiv.org/pdf/cs/0701193)." *Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI '03)*, 196–207. .