P. Cousot & R. Cousot, Vérification statique de la cohérence dynamique des programmes

Patrick Cousot & Radhia Cousot.
Vérification statique de la cohérence dynamique des programmes $fran\347ais$
In Rapport du contrat IRIA SESORI N^o 75-035, Laboratoire IMAG, University of Grenoble, France. 125 pages. 23 September 1975.
PDF (10.8 Mb), readable by Acrobate Reader.
Abstract: This is the first typeset report on abstract interpretation with an abstraction (def. 1, denoted @), a concretization (def. 4) and a widening (def. 14, ∇), their axiomatization in lattice theoretic terms (§ 2.1, ⊥ is denoted by a quad), an analysis algorithm (§ 2.6) for imperative programs (§ 2.4, formalized as flowcharts with cutnodes for widening) using concrete and abstract values (§ 2.2), concrete and abstract environments (§ 2.3, called abstract contexts) and transformers for assignments and tests (§ 2.5). The static analysis algorithm (p. 57) is proved to be terminating (§ 2.7) and sound (§ 2.8). Examples include intervals, pointer analysis, parity analysis.

\bibitem{CousotCousot-SESORI-1975}
P{.} Cousot and R{.} Cousot.
\newblock Vé\-ri\-fi\-ca\-tion  sta\-ti\-que de la co\-hé\-ren\-ce 
          dy\-na\-mi\-que des pro\-gram\-mes.
\newblock {Rap\-port du con\-trat IRIA SESORI No 75-035, 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.  23 Sep{.} 1975, 125 p.

@techreport{CousotCousot-SESORI-1975,
   author =      {Cousot, P{.} and Cousot, R{.}},
   title =       {Vé\-ri\-fi\-ca\-tion  sta\-ti\-que de la co\-hé\-ren\-ce 
                  dy\-na\-mi\-que des pro\-gram\-mes},
   institution = {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},
   type =        {{R}es{.} rep{.}},
   number =      {Rap\-port du con\-trat IRIA SESORI No 75-035},
   address =     {{G}re\-no\-ble, France},
   month =       {23 Sep{.}},
   year =        1975,
   note =        {125 p{.}},
}

droits d'auteur, copyright notice

Retour à / back to: Publications/Papers, Exposés/Talks, Index, Institutions, Enseignement / Teaching, Recherche / Research, Services

Email: cousot@di.ens.fr, cousotp@acm.org

Dernière mise à jour / Last modified : Tue Dec 3 14:02:31 CET 2002