An abstract interpreter doesn't run your program — it runs a blurred version of it, over and over, until the blur stops moving. That resting point is the fixpoint, and everything sound your analysis will ever say lives there.
This post tries to make that sentence feel obvious rather than mystical.
Running a program without running it
Take a loop that increments a counter. A concrete execution sees 0, 1, 2, 3, … — one state at a time, forever if it has to. An abstract execution sees sets of states, described in some restricted language: intervals, signs, parities. Instead of x = 3 it tracks x ∈ [0, +∞).
The analysis then asks a strange question: if I push this blurred state through the loop body once more, does it change?
# iterate until nothing changes
while state != state.step():
state = widen(state, state.step())
When the answer is no, you've reached a fixpoint. Nothing the program can do will escape the description you've computed. That is the entire trick — soundness is just "the blur is guaranteed to contain reality."
Why widening exists
Intervals can climb forever: [0,1], [0,2], [0,3], … The naive iteration never terminates, because the lattice has infinite ascending chains. Widening is the deliberately crude fix: when a bound keeps growing, give up and jump it to infinity.
NOTEWidening is what makes the loop terminate — and what makes the answer approximate. You trade precision for a promise it ends.
That trade is not a footnote; it is abstract interpretation. Every practical analyzer sits somewhere on the curve between "precise but divergent" and "terminating but useless," and widening operators are the knob.
Where soundness quietly ends
The theory guarantees the fixpoint over-approximates all behaviors of the semantics you modeled. Real tools model less than they imply: undefined behavior, concurrency, inline assembly, dlopen. The fixpoint is still a fixpoint — of a program that is not quite yours.
Knowing exactly which program your analyzer actually analyzed is, in practice, the difference between reading its output and believing it.