Abstract interpretation, developed by Patrick and Radhia Cousot in 1977, is a mathematical framework for sound static analysis of programs. It replaces the concrete (exact) semantics of a program with an abstract semantics that computes over simplified abstract values — such as replacing integers with their signs (+, -, 0) or with numeric intervals [lo, hi]. The abstraction is connected to the concrete semantics by a Galois connection ensuring soundness: every property proved in the abstract domain genuinely holds in the concrete program. The tradeoff is precision — the analysis may report false alarms (properties it cannot confirm) but never misses real violations.
Program analysis aims to determine properties of programs without running them — does this variable ever become negative? Can this array access go out of bounds? Can this pointer be null? Exact analysis is undecidable (Rice's theorem), so practical tools must approximate. Abstract interpretation provides the mathematical foundation for sound approximation: you can simplify the analysis as much as needed for tractability, as long as you never conclude that a property holds when it does not.
The framework is built on abstract domains connected to the concrete semantics by Galois connections. The concrete domain is the set of all possible program states (e.g., all possible integer values of a variable). An abstract domain replaces this with a simpler set. The sign domain {+, -, 0, top, bottom} represents integers by their sign, losing the exact value. The interval domain [lo, hi] tracks numeric bounds. The octagon domain tracks constraints of the form +/-x +/- y <= c. Each domain trades precision for efficiency. The Galois connection formalizes the correspondence: the abstraction function alpha maps concrete sets to their best abstract approximation, and the concretization function gamma maps abstract values to the concrete sets they represent. Soundness requires that the abstract computation always returns a result whose concretization contains all concrete possibilities.
Analyzing loops requires computing fixed points in the abstract domain. The analysis starts with an initial abstract state, applies the abstract transfer function for the loop body, and repeats until the result stabilizes. If the abstract domain has infinite ascending chains (the interval domain does: [0,1], [0,2], [0,3], ...), this iteration might not converge. Widening forces convergence by over-approximating: instead of computing the exact abstract union, the widening operator jumps to a safe over-approximation that breaks the ascending chain (e.g., replacing [0, n+1] with [0, +infinity]). This guarantees termination but may lose precision. Narrowing is a subsequent pass that recovers some precision by iterating downward from the widened result.
Abstract interpretation is the theoretical foundation of the most widely deployed static analysis tools. Astree, based on abstract interpretation with the octagon and polyhedra domains, proved the absence of runtime errors in Airbus A380 flight control software — covering 132,000 lines of C with zero false alarms after domain-specific tuning. Facebook/Meta's Infer uses separation logic combined with abstract interpretation to find memory bugs in mobile apps at scale. Polyspace (MathWorks) uses abstract interpretation for MISRA-C compliance in automotive software. These tools analyze millions of lines of code automatically, producing sound guarantees about properties like division by zero, buffer overflow, and null dereference.
The key engineering decision in abstract interpretation is choosing the abstract domain. Simpler domains (signs, intervals) are fast but imprecise, producing many false alarms. Richer domains (octagons, polyhedra) are more precise but more expensive — the polyhedra domain has worst-case exponential cost. The practical art is finding a domain that is precise enough for the target property and efficient enough for the target codebase. Domain designers often create product domains combining multiple abstractions (e.g., intervals for individual variables plus octagons for variable relationships) to balance precision and cost.