P. Cousot, Semantic foundations of program analysis

Patrick Cousot.
Semantic Foundations of Program Analysis.
In Program Flow Analysis: Theory and Applications, S.S. Muchnick and N.D. Jones, editors, Chapter 10, pages 303--342. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, U.S.A., 1981.
PDF (1528 K), readable by Acrobate Reader.
Abstract: A program defines a dynamic discrete system that is a transition relation on states. In section 4, we set-up general mathematical methods useful in the task of analyzing the behavior of dynamic discrete systems. In order to make this mathematically demanding sections self-contained, lattice-theoretical theorems on fixed points of isotone or continuous maps are first introduced in a separate subsection. The main result of section 4 shows that the predicates characterizing the descendants of the entry states, the ascendants of the exit states, the states which lead to an error, and the states which cause the system to diverge are the least or greatest solution to forward or backward fixed point equations. This result is completed by the proof that whenever a forward equation (corresponding to postconditions) is needed, a backward equation (corresponding to preconditions) can be used instead, and vice-versa. Finally we show that when a set of states of the dynamic discrete system is partitioned, the forward and backward equation can be decomposed into a system of equations. Numerous examples of applications are given which provide for a very concise presentation and justification of classical or innovative program proving methods. Section 5 tailors the general mathematical techniques previously set up for analyzing the behavior of a deterministic discrete dynamic system to suit the particular case when the system is a program. Two main theorems make explicit the syntactic construction rules for obtaining the systems of semantic backward or forward equations from the text of a program. The facts that the extreme fixed points of these systems of semantic equations can lead to complete information about program behavior and that the backward and forward approaches are equivalent are illustrated on the simple introductory example.
In the second part we briefly survey our joint work with Radhia Cousot on the automatic synthesis of approximate invariant assertions for programs. Because of well-known insolvability problems, the semantics equations which have been used in section 5 for program analysis cannot be algorithmically solved. hence we must limit ourselves to constructive methods which automatically compute approximate solutions? Such approximate information about the program behavior is often useful, e.g., in program verification systems, program debugging systems, optimizing compilers, etc. Approximate solutions to the semantic equations can be obtained by first simplifying these equations and next solving the simplified equations associated with the program text, using any chaotic iteration technique. In section 6.2 we show that when the exact solution to the simplified equations is obtained only after an infinite number of iteration steps, the convergence of the iterates can be sped up using an extrapolation technique based on a widening or narrowing operator. A hierarchy of examples illustrates the approximate program analysis method.

\bibitem{Cousot81-1}
P{.} Cousot.
\newblock Semantic foundations of program analysis.
\newblock In S.S{.} Muchnick and N.D{.} Jones, editors, \emph{Program Flow
  Analysis: Theory and Applications}, chapter~10, pages 303--342.
  Prentice-Hall, Inc{.}, Englewood Cliffs, New Jersey, {\sc usa}, 1981.

@incollection{Cousot81-1,
   author =    {Cousot, P{.}},
   title =     {Semantic Foundations of Program Analysis},
   pages =     {303--342},
   editor =    {Muchnick, S.S{.} and Jones, N.D{.}},
   chapter =   10,
   booktitle = {Program Flow Analysis: Theory and Applications},
   publisher = {Prentice-Hall, Inc{.}, Englewood Cliffs, New Jersey},
   year =      1981,
}

Most cited articles in Computer Science published in 1981

copyright notice
Last modified: Monday, 04-Jan-2010 12:31:56 CET