P. Cousot & R. Cousot, Induction principles for proving invariance properties of programs

Patrick Cousot & Radhia Cousot.
Induction principles for proving invariance properties of programs.
In «Tools & Notions for Program Construction: an Advanced Course», D. Néel (Ed.), Cambridge University Press, Cambridge, UK, pp. 75—119, August 1982.
PDF (5.3 Mb) (readable with Acrobat Reader)
Abstract: We propose sixteen sound and complete induction principles for proving program invariance properties. We study their relationships and show that they can be derived from each other by commuting mathematical tranformations. Only five of these induction principles correspond to already known invariance proof methods. We choose a non-conventional induction principle and construct corresponding partial correctness, non-termination and clean-behavior proof methods. When constructing these new proof methods, we informallty apply CousotCousot[80b] mathematical approach. This essentially consists in decomposing the global inductive invariant involved in the induction principle into an equivalent set of local invariants and in deriving the corresponding verification conditions.

Bibliography:

\bibitem{CousotCousot82-TNPC}
P{.} Cousot and R{.} Cousot.
\newblock Induction principles for proving invariance properties of programs.
\newblock In \emph{Tools \& Notions for Program Construction: an Advanced
          Course}, D{.} N{\'e}el (Ed.), Cambridge University Press, Cambridge, UK,
          pp{.} 75--119, August 1982.

@inproceedings{CousotCousot82-TNPC,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Induction principles for proving invariance properties of
                programs},
   booktitle = {Tools \& Notions for Program Construction: an Advanced Course},
   editor =    {D{.} N{\'e}el},
   publisher = {Cambridge University Press, Cambridge, UK},
   pages =     {75--119},
   month =     aug,
   year =      {1982},
}

copyright notice
Last modified: Monday, 04-Jan-2010 13:31:42 CET