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)¹.

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). 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 — its Eva plugin is an abstract interpreter for C; part of a broader analysis platform.
• IKOS (NASA) — an LLVM-based engine for proving the absence of runtime errors in C/C++; and MOPSA (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: 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, 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: 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: 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)². 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 · Methods
• Formal methods · Methods
• Temporal-logic falsification · Methods
• Termination analysis · Methods
• Testing machine-learning systems · Methods
• Verifying memory safety · Methods
• Verifying numerical code · Methods
• Verifying safety-critical systems · Methods
• Worst-case execution-time analysis · Methods
• Conventional terminology · Conventional
• Glossary · Overview

References

---

1. Cousot, Patrick, and Radhia Cousot. 1977. "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints." Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '77), 238–52. https://doi.org/10.1145/512950.512973. ↩

2. Blanchet, Bruno, Patrick Cousot, Radhia Cousot, et al. 2003. "A Static Analyzer for Large Safety-Critical Software." Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI '03), 196–207. https://doi.org/10.1145/781131.781153. ↩