We present a general algorithm allowing most of these certifications to be done at compile time. The static analysis of a program consists of an abstract evaluation of the program (NAUR, SINTZOFF, KILDALL, WEGBREIT, KARR) which computes, by successive approximations, an abstract context at every program point. A context is a set of pairs (identifier, abstract value). An abstract value denotes a set of execution values or properties of it, satisfying a number of dynamic conditions. An abstract interpretor defines the sequencing of abstract evaluation through the different paths of the program, and builds a union of contexts resulting from the junction of these paths. The elementary interpretation of basic operations of the language and the choice of abstract values are left unspecified. They depend only upon the specified dynamic properties of variables which have been chosen for being extracted from the program. The correctness and termination of the abstract evaluation algorithm, rely only on the algebraic structure of the abstract value set, and on some properties of abstract basic opertions. Several abstract evaluations can be defined for a program, in order to elminate redundant tests, verify correct uses of operations, choose types or organization of data structures in the case of very high level languages or provide diagostic information.

\bibitem{CousotCousot-IMAG-RR25-1975}
P{.} Cousot and R{.} Cousot.
\newblock Static verification of dynamic type properties of variables.
\newblock {R}es{.} rep{.} R.R{.} 25, 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.  Nov{.} 1975, 18 p.

@techreport{CousotCousot-IMAG-RR25-1975,
   author =      {Cousot, P{.} and Cousot, R{.}},
   title =       {Static Verification of Dynamic Type Properties of Variables},
   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 =      {R.R{.} 25},
   address =     {{G}re\-no\-ble, France},
   month =       {Nov{.}},
   year =        1975,
   note =        {18 p{.}},
}