Abstract Interpretation
A static-analysis framework that computes safe abstractions of concrete program executions to reason about selected program properties.
Technical Context
Abstract interpretation represents concrete program states in domains such as intervals, signs or relational numeric abstractions. A sound over-approximation covers every concrete behavior relevant to the property being analyzed, while potentially introducing states that no real execution can reach.
Fixed-point iteration, widening and narrowing, and the selected abstract domains determine both precision and computational cost.
Boundaries
A strong guarantee is meaningful only when the analyzed property, language semantics and environment assumptions are explicit. Abstract interpretation does not make arbitrary program properties decidable.