Prove a property without running the program — compute on shapes instead of exact values, and never claim more than you can cover. A program that adds and multiplies unknown numbers is analysed in the rule of signs — Cousot's own example — where every concrete run is guaranteed to land inside the abstract answer. Down the center, data flows: an abstract input goes in, the abstract semantics compute, a sound over-approximation comes out. The blue team proves it covers every real behaviour; the red team under-approximates to break it.
source P. Cousot & R. Cousot, Abstract Interpretation: a unified lattice model…, POPL '77, pp. 238–252 — di.ens.fr/~cousot/COUSOTpapers/POPL77. Rendered, not quoted.
The concrete world is sets of integers; the abstract world is signs. Eight abstract values, ordered by subset: ⊥ ⊑ {neg},{zero},{pos} ⊑ {≤0},{≠0},{≥0} ⊑ ⊤. Two maps bind the worlds:
α (abstraction) sends a set to the signs it contains. γ (concretization) sends a sign-set back to every integer of that sign. They are adjoint: α(X) ⊑ a ⟺ X ⊆ γ(a), with α(γ(a))=a. The rule of signs (Cousot's example) gives exact abstract operators:
| × | neg | zero | pos |
|---|---|---|---|
| neg | pos | zero | neg |
| zero | zero | zero | zero |
| pos | neg | zero | pos |
| + | neg | zero | pos |
|---|---|---|---|
| neg | neg | neg | ⊤ |
| zero | neg | zero | pos |
| pos | ⊤ | pos | pos |
neg + pos = ⊤: addition of opposite signs genuinely loses information. Live for the panel's input: γ(x#) = , and α of the real results = .
Cousot's move is that a sound over-approximation is a proof: if no real behaviour escapes the abstract answer, then any property the abstract answer guarantees, the real program has. You never ran every input — you covered them all.
That is the door into the model checking: an infinite-state system is undecidable to check exactly, but its abstraction is finite and decidable. Over-approximate, check the abstraction, and a proof there is a proof here. Each sphere is the next one's premise — honesty by never claiming more than it can cover.
The blue team's live check: re-run soundness over all 8 abstract inputs, confirm the Galois adjunction, and confirm widening terminates. If red under-approximates, this badge is where it shows.
One tiny program with an unknown input x:
Instead of a number, you feed x a shape — one of the eight sign-sets (its abstract value x#). The concrete universe here is the integers −3…3, small enough to check every real run exhaustively. The panel computes the abstract answer and confronts it with all the real ones.
Change the shape — the abstract answer is recomputed from the rule-of-signs operators, and every concrete run in γ(x#) is executed and confronted. Nothing is looked up.
| concrete x | b = x·x + x | sign |
|---|
SOUNDNESS = α(real results) ⊑ abstract result. It may be strictly wider (a spurious sign) — that is legal. It may never be narrower — that would drop a real behaviour.
What the machine produces, proven: for every one of the 8 abstract inputs the real behaviour is contained in the abstract answer — 8/8 sound, of which are strict over-approximations (spurious signs added, none dropped) and are exact. The interval fixpoint with widening reaches in steps, where plain iteration never stops.
The blue team's witness (left) confirms these numbers live; the red team (right) tries to make a real value escape.
And exactness is out of reach on principle: by Rice's theorem no analysis decides every non-trivial property of every program. So the abstract answer is a choice of domain — signs, intervals, octagons, polyhedra — each trading cost for precision. The framework guarantees you don't lie; it cannot guarantee you say anything useful.
"Abstract interpretation proves the program correct." Cut. It proves a property holds, soundly. It also raises false alarms; a clean run is a proof, a warning may be spurious.
"More abstract values = more precise." Cut. A finer domain is more precise but may not terminate — infinite ascending chains need widening, which deliberately over-shoots to converge.
"α and γ are inverses." Kept, corrected. They form a Galois connection, not a bijection: α(γ(a))=a here, but X ⊆ γ(α(X)) is generally strict — abstraction loses, and that loss is the whole point.
The red team's move: swap one sound operator for an under-approximation — make pos · pos drop the reachable pos. Now the abstract answer is too small and a real result escapes it. The blue team's witness (window 7) is watching.
Drop one reachable abstract value and soundness fails: the concrete pos result of x·x+x for a positive x is no longer covered — the witness recomputes, finds a real behaviour uncovered, and turns red. Nothing is faked; the attack is real and it is caught.