P. Cousot & R. Cousot, Towards a Universal Model for Static Analysis of Programs

Patrick Cousot & Radhia Cousot.
Towards a Universal Model for Static Analysis of Programs.
Unpublished manuscript, Laboratoire IMAG, University of Grenoble, France. 90 pages. January 1977.
PDF (3.87 Mb), readable by Acrobate Reader.
Abstract: The abstract interpretation of programs is a mathematical model for static analysis of programs :
     A new interpretation is given to the program text and this allows the building of a system of equations. The analysis of the program then consists in verifying that a solution provided by the user is correct, or in computing this solution, or else in discovering a good approximation of this solution.
     The abstract interpretation of programs was formalized in Cousot and Cousot [1977]. Only a few lattice theoretical results are recalled here for the paper to be self-contained.
     Our main purpose is to show that most program analysis techniques may be understood and modelled as abstract interpretatiobs of programs. This is illustated by the following examples :
- Global data flow analysis,
- Analysis of program performance,
- Denotational semantics of programs,
- Proofs of program partial correctness,
- proofs of program termination,
- Symbolic execution of programs,
- Type verification/discovery,
- Finite/infinite state program analysis.
The application of abstract interpretation in studying these apparently unrelated techniques renders the connexion between them clear and straightforward. Moreover, numerous mis-understood problems are highlighted when explained by the model of abstract interpretation.

Bibliographic reference:

\bibitem{CousotCousot-Unpublished-TUMSAP-1977}
P{.} Cousot and R{.} Cousot.
\newblock Towards a universal model for static 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.  Jan{.} 1977, 90 p.

@unpublished{CousotCousot-Unpublished-TUMSAP-1977,
   author = {Cousot, P{.} and Cousot, R{.}},
   title = {Towards a Universal Model for Static 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, 90 p{.}},
   month =  {Jan{.}},
   year =   1977,
}

copyright notice
Last modified: Wed Dec 4 12:42:43 MET 2002