Section 3 describes the syntax and mathematical semantics of a simple flowchart language, Scott and Strachey[71]. This mathematical semantics is used in section 4 to built a more abstract model of the semantics of programs, in that it ignores the sequencing of control flow. This model is taken to be the most concrete of the abstract interpretations of programs. Section 5 gives the formal definition of the abstract interpretations of a program. Abstract program properties are modeled by a complete semilattice, Birkoff[61]. Elementary program constructs are locally interpreted by order-preserving functions which are used to associate a system of equations with a program. The program global properties are then defined as one of the extreme fixpoints of that system, Tarski[55]. The abstraction process is defined in section 6. It is shown that the program properties obtained by an abstract interpretation of a program are consistent with those obtained by a more refined interpretation of that program. In particular, an abstract interpretation may be shown to be consistent with the formal semantics of the language. Levels of abstraction are formalized by showing that consistent abstract interpretations form a lattice (section 7). Section 8 gives a constructive definition of abstract properties of programs based on constructive definitions of fixpoints. It shows that various classical algorithms such as Kildall[73], Wegbreit[75], compute program properties as limits of finite Kleene[52]'s sequences. Section 9 introduces finite fixpoint approximation methods to be used when Kleene's sequences are infinite, Cousot[76]. They are shown to be consistent with the abstraction process. Practical examples illustrate the various sections. The conclusion points out that the abstract interpretation of programs is a unified approach to apparently unrelated program analysis techniques.
\bibitem{CousotCousot77-1} P{.} Cousot and R{.} Cousot. \newblock Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. \newblock In \emph{Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, pages 238--252, Los Angeles, California, 1977. ACM Press, New York, NY, USA. @inproceedings{CousotCousot77-1, author = {Cousot, P{.} and Cousot, R{.}}, title = {Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints}, pages = {238--252}, booktitle = {Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, address = {Los Angeles, California}, publisher = {ACM Press, New York, NY}, year = 1977, }