Abstract Interpretation

Origin. Cousot and Cousot introduced abstract interpretation (1977). Framework for sound approximation of program semantics. Abstract domains capture properties of interest. Galois connections formalize soundness. Foundation for static analysis tools (Astrée, Polyspace, Infer).

Models. Sound approximation of semantics. Concrete semantics: exact program behavior (often infinite). Abstract semantics: finite approximation preserving properties. Over-approximation: if abstract says "may error," concrete may or may not. Under-approximation: if abstract says "definitely errors," concrete does. Soundness via Galois connections.

Formalism.

Galois connection: (C, ⊑) ⇄ (A, ⊑) α ↓ γ

• C: concrete domain (e.g., sets of states)
• A: abstract domain (e.g., intervals)
• α: C → A (abstraction) — extract property
• γ: A → C (concretization) — what abstract represents
• Galois: α(c) ⊑ a iff c ⊑ γ(a)

Soundness: Abstract transformer F♯ is sound if: α ∘ F ⊑ F♯ ∘ α Concrete computation followed by abstraction ⊑ abstract directly.

Common abstract domains:

• Signs: {-, 0, +, ⊤}
• Intervals: [l, u] where l ≤ n ≤ u
• Octagons: ±x ± y ≤ c
• Polyhedra: linear inequalities

Fixed points: Loops = fixed points: lfp(F) = ⊔{Fⁿ(⊥) : n ∈ ℕ} Widening ∇: ensure termination by jumping to fixed point. Narrowing △: improve precision after widening.

Reduced product: Combine domains: A₁ × A₂ with reduction. More precise than either alone.

Symbols.

Metatheory. Cousot and Cousot (POPL 1977) established the fixpoint transfer theorem that carries the framework: if (α, γ) is a Galois connection between concrete and abstract lattices and the abstract transformer satisfies F♯ ⊒ α ∘ F ∘ γ, then lfp F♯ over-approximates α(lfp F), so one abstract fixpoint is a sound statement about every concrete execution. The composite α ∘ F ∘ γ is the best abstract transformer, the most precise sound one, and it exists exactly when the Galois connection does. Galois connections compose, which is what makes analyses modular. Their 1979 sequel organized abstract domains into a lattice ordered by precision, with reduced product and disjunctive completion as operations on it. Completeness is not automatic but is repairable: Giacobazzi, Ranzato and Scozzari (2000) showed that every domain has a most abstract complete refinement, its complete shell, and a most concrete complete abstraction, its core, each definable as a fixpoint.

Applies to. Industrial static analyzers (Astrée in Airbus). Bug finding (null pointers, buffer overflows). Compiler optimization (constant propagation = abstract interpretation). Security (taint analysis). Termination analysis. Shape analysis (heap structures).

Limitations. Soundness together with guaranteed termination forces incompleteness: by Rice's theorem no terminating analysis decides a nontrivial semantic property, so an over-approximating analysis necessarily reports alarms that no execution realizes, and the alarm rate is a design parameter rather than a defect to be removed. Widening is not monotone — a more precise abstract input can yield a less precise fixpoint — so precision does not compose and there is no canonical widening operator. Some useful domains admit no abstraction function at all: an arbitrary set of points has no smallest enclosing convex polyhedron, so the Galois connection must be abandoned for concretization-only soundness, and the best-transformer result goes with it. Relational domains' precision has a measured cost — octagons cubic and polyhedra worst-case exponential in the number of variables, which is why both are applied to small variable packs rather than whole programs.

© 2026 Lingenic LLC