Abstract interpretation analyzes all possible program executions using a simplified domain of facts instead of concrete runtime values.

Suppose a variable can contain any integer, but an analysis only cares about sign. Concrete values are mapped into an abstract domain such as

$${\text{Negative},\text{Zero},\text{Positive},\text{Unknown}}.$$

Instead of evaluating x * x for every integer $x$, the abstract semantics can infer that the result is never negative.

At a control-flow join, information from alternative paths must be safely combined. If one branch makes $x$ positive and another makes it negative, the joined fact may become Unknown rather than choosing one unsoundly.

The central requirement is sound over-approximation: the abstract result must include every behavior possible in the concrete program, even if it also includes impossible behaviors. This permits false positives but prevents the analysis from proving safety by silently omitting a real execution.

Loops are handled by computing fixed points of abstract transfer functions. Because some abstract domains contain infinite ascending chains, widening can force convergence at the cost of precision.

Abstract interpretation provides a mathematical framework behind many static analyses: interval analysis, nullness checking, possible-value analysis, pointer analysis and parts of security analysis all fit the same pattern of executing a program over an abstract domain.