Abstract interpretation, first formalised by Cousot and Cousot in 1977 [CC77], executes a program on an abstract machine to determine the properties of interest [vJ11, p. 1255].
The level of detail in the abstract machine specification typically determines the accuracy of the results.
At one end of the spectrum is an abstract machine that faithfully represents the concrete semantics of the language.
Abstract interpretation on such a machine 👆 would correspond to a concrete execution on the real machine.
Typical abstract interpretation analyses, however, do not require detailed semantics.
A bit of theory
Fundamentally, the correctness problem of a program is undecidable, so approximation is necessary [Cou01, Abstract].
The purpose of abstract interpretation is to formalise this idea 👆 of approximation; see Fig. 1.
Formally, abstract interpretation is founded in the theory for approximating sets and set operations [Cou01, Sec. 2].
The semantics of a program can be defined as the solution to a fixpoint (short for fixed point) equation.
Thus, an essential role of abstract interpretation is providing constructive and effective methods for fixpoint approximation and checking by abstraction.
By observing computations at different levels of abstraction (trace semantics → relational semantics → denotational semantics → weakest precondition semantics → Hoare logics), fixpoints can be approximated.
Fig. 1: In abstract interpretation, the program analyzer computes an approximate semantics of the program [Cou01, Fig. 12].
The generator generates equations/constraints, the solution to which is a computer representation of the program semantics.
The solver solves these equations/constraints.
The diagnoser checks the solutions with respect to the specification and outputs “yes”, “no” or “unknown”.
References
[Cou01]
P. Cousot, Abstract Interpretation Based Formal Methods and Future Challenges, pp. 138–156, Springer Berlin Heidelberg, Berlin, Heidelberg, 2001. https://doi.org/10.1007/3-540-44577-3_10.
[CC77]
P. Cousot and R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, in Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’77, Association for Computing Machinery, 1977, pp. 238–252. https://doi.org/10.1145/512950.512973.
