Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Summaries for while programs with recursion

Wagner, Silke

MPI-I-2004-2-007. December 2004, 22 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
Procedure summaries are an approximation of the effect of a
procedure call. They have been used to prove partial correctness and
safety properties. In this report, we introduce a generalized notion of
procedure summaries and present a framework to verify total correctness
and liveness properties of a general class of while programs with
recursion. We provide a fixpoint system for computing summaries, and a
proof rule for total correctness of a program given a summary. With
suitable abstraction methods and algorithms for efficient summary
computation, the results presented here can be used for the automatic
verification of termination and liveness properties for while programs
with recursion.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-2004-2-007.pdfMPI-I-2004-1-007.ps213 KBytes; 112 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Wagner, Silke},
  TITLE = {Summaries for while programs with recursion},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-2004-2-007},
  MONTH = {December},
  YEAR = {2004},
  ISSN = {0946-011X},