P. Cousot, Analysis of the behavior of dynamic discrete systems, Part I: deterministic systems

Analysis of the behavior of dynamic discrete systems, Part I: deterministic systems.
In Research Report R.R. 161, Laboratoire IMAG, University of Grenoble, France. 34 pages. Janvier 1979.
PDF (5.4 Mb), readable by Acrobate Reader.
Abstract: We establish general mathematical techniques for analyzing the behavior of deterministic dynamic discrete systems. In order to illustrate a possible application of these results, we consider the problem of analyzing semantic properties of programs, that is, the particular case when the dynamic discrete system is defined by a sequential program.
Keywords and Phrases: dynamic discrete system, fixed points, descendants of the entry states, ascendants of the exit states, states not leading to an error, pre, post, partitioned dynamic system, system of forward equations, system of backward equations, forward analysis, backward analysisf backward equations.
Note: this research report was later partially published as
Patrick Cousot. Semantic foundations of program analysis. In S.S. Muchnick & N.D. Jones, editors, Program Flow Analysis: Theory and Applications, Ch. 10, pages 303—342, Prentice-Hall, Inc., Englewood Cliffs, New Jersey, U.S.A., 1981.

\bibitem{Cousot-IMAG-RR161-1979}
P{.} Cousot.
\newblock Analysis of the behavior of dynamic discrete systems, 
          Part I: deterministic systems
\newblock {R}es{.} rep{.} R.R{.} 161, 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{.} 1979, 34 p.

@techreport{Cousot-IMAG-RR161-1979,
   author =      {Cousot, P{.}},
   title =       {Analysis of the behavior of dynamic discrete systems, 
                  Part I: deterministic systems},
   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{.} 161},
   address =     {{G}re\-no\-ble, France},
   month =       {Jan{.}},
   year =        1979,
   note =        {34 p{.}},
}

copyright notice
Last modified: Tue Dec 3 14:02:31 CET 2002