P. Cousot & R. Cousot, Abstract interpretation and application to logic programs

Patrick Cousot & Radhia Cousot.
Abstract interpretation and application to logic programs.
Journal of Logic Programming, 13(2--3):103--179, 1992.
Note: the publisher of JLP published the Galley proofs thus making the paper unreadable, here is the original manuscript.
MR 93g:68073 (Reviewer: F. J. van der Linden) 68Q55 (68N17)
Paper: PDF (1.2 MB)
Abstract: Abstract interpretation is a theory of semantics approximation which is used for the construction of semantics-based program analysis algorithms (sometimes called ``data flow analysis''), the comparison of formal semantics (e.g. construction of a denotational semantics from an operational one), the design of proof methods, etc.
Automatic program analysers are used for determining statically conservative approximations of dynamic properties of programs. Such properties of the run-time behavior of programs are useful for debugging (e.g. type inference), code optimization (e.g. compile-time garbage collection, useless occur-check elimination), program transformation (e.g. partial evaluation, parallelization) and even program correctness proofs (e.g. termination proof).
After a few simple introductory examples we recall the classical framework for abstract interpretation of programs. Starting from a standard operational semantics formalized as a transition system, classes of program properties are first encapsulated in collecting semantics expressed as fixpoints on partial orders representing concrete program properties. We consider invariance properties characterizing the descendant states of the initial states (corresponding to top/down or forward analyses), ascendant states of the final states (corresponding to bottom/up or backward analyses) as well as a combination of the two. Then we choose specific approximate abstract properties to be gathered about program behaviors and express them as elements of a poset of abstract properties. The correspondence between concrete and abstract properties is established by a concretization and abstraction function which is a Galois connection formalizing the loss of information. We can then constructively derive the abstract program properties from the collecting semantics by a formal computation leading to a fixpoint expression in terms of abstract operators on the domain of abstract properties. The design of the abstract interpreter then involves the choice of a chaotic iteration strategy to solve this abstract fixpoint equation. We insist on the compositional design of this abstract interpreter which is formalized by a series of propositions for designing Galois connections (such as Moore families, decomposition by partitioning, reduced product, down-set completion, etc.). Then we recall the convergence acceleration methods using widening and narrowing allowing for the use of very expressive infinite domains of abstract properties.
We show that this classical formal framework can be applied in extenso to logic programs. For simplicity we use a variant of SLD-resolution as the standard operational semantics. The first example is groundness analysis which is a variant of Mellish mode analysis. It is extended to a combination of top/down and bottom/up analyses. The second example is the derivation of constraints among argument sizes which involves an infinite abstract domain requiring the use of convergence acceleration methods. We end up with a short thematic guide to the literature on abstract interpretation of logic programs.

\bibitem{CousotCousot92-1}
P.~Cousot and R.~Cousot.
\newblock Abstract Interpretation and Application to Logic Programs.
\newblock \emph{Journal of Logic Programming}, 13(2--3):103--179, 1992.

@article{CousotCousot92-1,
   author =  {Cousot, P{.} and Cousot, R{.}},
   title =   {Abstract Interpretation and Application to Logic Programs},
   pages =   {103--179},
   journal = {Journal of Logic Programming},
   year =    1992,
   volume =  13,
   number =  {2--3},
   note =    {{\footnotesize (The editor of Journal of Logic Programming{} has mistakenly published the
              unreadable galley proof. For a correct version of this paper, see
              \url{http://cs.nyu.edu/~pcousot/}.)}},
}

Most cited articles in Computer Science published in 1992

copyright notice
Last modified: Friday, 04-May-2012 15:18:20 EDT