Abstract Interpretation
Abstract interpretation approximates program semantics over an abstract domain, soundly proving program properties (e.g., no division by zero, no array out-of-bounds access).
Purpose
Soundly prove that a program is free of a certain class of defects — a practical approximation method for formal verification.
Mechanism
Maps concrete semantics into an abstract domain (intervals, signs, octagons) and computes a fixpoint on that domain. Over-approximation guarantees soundness (reports true defects but may produce false positives). Sonar and Astrée use this to analyze flight-control software.
Use cases
- Formal verification
- Defect proof
- Safety-critical software