Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Podelski, Andreas
Schaefer, Ina
Wagner, Silke

dblp
dblp
dblp



Editor(s):

Sagiv, Mooly

dblp

Not MPII Editor(s):

Sagiv, Mooly

BibTeX cite key*:

PSW:05

Title, Booktitle

Title*:

Summaries for While Programs with Recursion

Booktitle*:

Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005

Event, URLs

URL of the conference:

http://www.etaps05.inf.ed.ac.uk/

URL for downloading the paper:

http://www.mpi-sb.mpg.de/~swagner

Event Address*:

Edinburgh, UK

Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

4 April 2005

Event End Date:

8 April 2005

Publisher

Name*:

Springer

URL:

http://www.springer.de

Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

3444

Number:


Month:

April

Pages:

94-107

Year*:

2005

VG Wort Pages:


ISBN/ISSN:

3-540-25435-8

Sequence Number:


DOI:




Note, Abstract, ©


(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 paper, 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.

Keywords:

Recursive Programs, Summaries, Total Correctness, Program Analysis, Program Verification



Download
Access Level:

Intranet

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, VG Wort, CCL bibliography



BibTeX Entry:

@INPROCEEDINGS{PSW:05,
AUTHOR = {Podelski, Andreas and Schaefer, Ina and Wagner, Silke},
EDITOR = {Sagiv, Mooly},
TITLE = {Summaries for While Programs with Recursion},
BOOKTITLE = {Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005},
PUBLISHER = {Springer},
YEAR = {2005},
VOLUME = {3444},
PAGES = {94--107},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Edinburgh, UK},
MONTH = {April},
ISBN = {3-540-25435-8},
}


Entry last modified by Silke Wagner, 01/28/2008
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)
Silke Wagner
Created
03/08/2005 04:16:05 PM
Revisions
2.
1.
0.

Editor(s)
Silke Wagner
Christine Kiesel
Silke Wagner

Edit Dates
08.03.2006 14:53:07
27.04.2005 10:25:36
08.03.2005 16:16:05