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.

Symbol	Unicode	Name	Meaning
α	U+03B1	Abstraction	Concrete to abstract
γ	U+03B3	Concretization	Abstract to concrete
⊑	U+2291	Ordering	Less precise
⊔	U+2294	Join	Least upper bound
⊓	U+2293	Meet	Greatest lower bound
∇	U+2207	Widening	Force termination
△	U+25B3	Narrowing	Improve precision
⊤, ⊥	U+22A4, U+22A5	Top, Bottom	Unknown, unreachable

Metatheory. Soundness: abstract interpretation never misses errors (for over-approximation). Completeness: achievable for specific properties. Termination: widening guarantees finite iterations. Precision/cost tradeoff: more precise domains cost more. Galois connections compose: (A₁ ⇄ A₂) ∘ (A₂ ⇄ A₃) = (A₁ ⇄ A₃).

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. Over-approximation causes false positives. Domain design is an art. Widening loses precision. Interprocedural analysis is expensive. Relational domains (polyhedra) don't scale naively. Requires expertise to tune for specific programs.