MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments

MPI-I-2004-2-007

Summaries for while programs with recursion

Wagner, Silke

December 2004, 22 pages.

.
Status: available - back from printing

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.

  • MPI-I-2004-2-007.pdfMPI-I-2004-1-007.ps
  • Attachement: 85998158.ps (213 KBytes); MPI-I-2004-2-007.pdf (112 KBytes)

URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2004-2-007

Hide details for BibTeXBibTeX
@TECHREPORT{PodelskiSchaeferWagner2004,
  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},
}