Technical, Research Report
@TechReport
Technischer-, Forschungsbericht


Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:









Author, Editor
Author(s):
Podelski, Andreas
Schaefer, Ina
Wagner, Silke		dblp
dblp
dblp
Editor(s):

BibTeX Citekey*:

PodelskiSchaeferWagner2004

Language:

English

Title, Institution

Title*:

Summaries for While Programs with Recursion

Institution*:

Max-Planck-Institut für Informatik

Publishers or Institutions Address*:

Stuhlsatzenhausweg 85, 66123 Saarbrücken, Germany

Type:

Research Report

No, Year, pp.,

Number*:

MPI-I-2004-2-007
Pages*:

22

Month:

December
VG Wort
Pages*:


Year*:

2004
ISBN/ISSN:

0946-011X





DOI:




Note, Abstract, ©

Note:


(LaTeX) Abstract:

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.

Categories / Keywords:


Copyright Message:


HyperLinks / References / URLs:


Personal Comments:


File Upload:


Download
Access Level:

Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
popular
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat


BibTeX Entry:
@TECHREPORT{PodelskiSchaeferWagner2004,
AUTHOR = {Podelski, Andreas and Schaefer, Ina and Wagner, Silke},
 TITLE = {Summaries for While Programs with Recursion},
 PUBLISHER = {AG 2 - Ganzinger},
 YEAR = {2004},
 TYPE = {Research Report},
 INSTITUTION = {Max-Planck-Institut für Informatik},
 NUMBER = {MPI-I-2004-2-007},
 PAGES = {22},
 ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
 MONTH = {December},
 ISBN = {0946-011X},
}

Entry last modified by Silke Wagner, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Created
08/12/2005 12:08:53 PM
Revisions
2.
1.
0.

Editor(s)
Silke Wagner
Christine Kiesel


Edit Dates
08.03.2006 14:53:31
12.08.2005 12:10:59


Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section
MPI-I-2004-1-007.ps