P. Cousot & R. Cousot, Fixed Point Approach to the Approximate Semantic Analysis of Programs

Patrick Cousot & Radhia Cousot.
Fixed Point Approach to the Approximate Semantic Analysis of Programs.
Unpublished manuscript, Laboratoire IMAG, University of Grenoble, France. 48 pages. June 1977.
PDF (2.59 Mb)
Abstract: Abstract interpretation constitutes a mathematical model for static analysis of programs. The information to be gathered about programs are modeled in a complete lattice. According to the semantics of the utilized language, elementary instructions can be interpreted by order-preserving functions. This permits a system of recursive equations to be associated with any particular program. The determination of properties of that program then consists in solving the corresponding fixed point equations. For continuous equations, the exact solution can be constructed iteratively by Jacobi's successive approximations, but in practice any chaotic iteration method is shown to fit.
Standard arguments on decidability show that convergence of successive iterates may happen not to be guaranteed. Mathematical techniques are reviewed to cope with the determination of undecidable properties of programs. In particular, we introduce structural and more generally computational approximation methods which can always be used in practice to mechanically discover a correct approximation of the exact but unreachable solution to the equations.
Abstract interpretation of programs provides a unified approach to apparently unrelated program analysis techniques. It is shown to be powerful enough to tackle with theoretical as well as practical problems such as denotational semantics of programs, proofs of partial correctness, proofs of termination, symbolic execution, analysis of program performance, type verification or discovery, global data flow analysis, finite or infinite state program analysis.
Key Words and Phrases: abstract interpretations, static analysis, lattice, system of equations, fixed points construction, fixed points approximation, chaotic iterative methods, program semantics, logical analysis, correctness, termination,symbolic execution, performance analysis, type discovery, finite or infinite state program analysis, global data flow analysis.

Bibliographic reference:

\bibitem{CousotCousot-Unpublished-FP-1977}
P{.} Cousot and R{.} Cousot.
\newblock Fixed point approach to the approximate semantic analysis of
          programs.
\newblock Unpublished manuscript, La\-bo\-ra\-toi\-re IMAG,
          Uni\-ver\-si\-t{\'e} scien\-ti\-fi\-que et m{\'e}\-di\-ca\-le de
          Gre\-no\-ble, {G}re\-no\-ble, France.  June 1977, 48 p.

@unpublished{CousotCousot-Unpublished-FP-1977,
   author = {Cousot, P{.} and Cousot, R{.}},
   title =  {Fixed Point Approach to the Approximate Semantic Analysis of
             Programs},
   note =   {La\-bo\-ra\-toi\-re IMAG, Uni\-ver\-si\-t{\'e}
             scien\-ti\-fi\-que et m{\'e}\-di\-ca\-le de Gre\-no\-ble,
             {G}re\-no\-ble, France, 48 p{.}},
   month =  {June},
   year =   1977,
}

copyright notice
Last modified: Tue Dec 3 21:48:46 CET 2002