Inductive reasoning for shape invariants

Lilia Georgieva; Patrick Maier

Inductive reasoning for shape invariants

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Automatic verification of imperative programs that destructively manipulate heap data structures is challenging. In this paper we propose an approach for verifying that such programs do not corrupt their data structures. We specify heap data structures such as lists, arrays of lists, and trees inductively as solutions of logic programs. We use off-the-shelf first-order theorem provers to reason about these specifications.

Original language	English
Title of host publication	Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09)
Editors	Nicolas Peltier, Viorica Sofronie-Stokkermans
Place of Publication	Oslo
Publisher	University of Oslo
Pages	75-89
Number of pages	15
ISBN (Print)	82-7368-347-8
Publication status	Published - Jul 2009
Event	International Workshop on First-Order Theorem Proving, FTP 2009 - Oslo, Norway Duration: 6 Jul 2009 → 7 Nov 2012

Conference

Conference	International Workshop on First-Order Theorem Proving, FTP 2009
Country/Territory	Norway
City	Oslo
Period	6/07/09 → 7/11/12

Access to Document

http://ceur-ws.org/Vol-556/paper08.pdf

Cite this

@inproceedings{3b31d1c858cb4e20b86d310f943b5c6d,

title = "Inductive reasoning for shape invariants",

abstract = "Automatic verification of imperative programs that destructively manipulate heap data structures is challenging. In this paper we propose an approach for verifying that such programs do not corrupt their data structures. We specify heap data structures such as lists, arrays of lists, and trees inductively as solutions of logic programs. We use off-the-shelf first-order theorem provers to reason about these specifications.",

author = "Lilia Georgieva and Patrick Maier",

note = "Appeared in printed version as Research Report 386, University of Oslo, Department of Informatics, 2009, ISBN 82-7368-347-8, ISSN 0806-3036; International Workshop on First-Order Theorem Proving, FTP 2009 ; Conference date: 06-07-2009 Through 07-11-2012",

year = "2009",

month = jul,

language = "English",

isbn = "82-7368-347-8",

pages = "75--89",

editor = "Nicolas Peltier and Viorica Sofronie-Stokkermans",

booktitle = "Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09)",

publisher = "University of Oslo",

}

TY - GEN

T1 - Inductive reasoning for shape invariants

AU - Georgieva, Lilia

AU - Maier, Patrick

N1 - Appeared in printed version as Research Report 386, University of Oslo, Department of Informatics, 2009, ISBN 82-7368-347-8, ISSN 0806-3036

PY - 2009/7

Y1 - 2009/7

N2 - Automatic verification of imperative programs that destructively manipulate heap data structures is challenging. In this paper we propose an approach for verifying that such programs do not corrupt their data structures. We specify heap data structures such as lists, arrays of lists, and trees inductively as solutions of logic programs. We use off-the-shelf first-order theorem provers to reason about these specifications.

AB - Automatic verification of imperative programs that destructively manipulate heap data structures is challenging. In this paper we propose an approach for verifying that such programs do not corrupt their data structures. We specify heap data structures such as lists, arrays of lists, and trees inductively as solutions of logic programs. We use off-the-shelf first-order theorem provers to reason about these specifications.

M3 - Conference contribution

SN - 82-7368-347-8

SP - 75

EP - 89

BT - Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09)

A2 - Peltier, Nicolas

A2 - Sofronie-Stokkermans, Viorica

PB - University of Oslo

CY - Oslo

T2 - International Workshop on First-Order Theorem Proving, FTP 2009

Y2 - 6 July 2009 through 7 November 2012

ER -

Inductive reasoning for shape invariants

Abstract

Conference

Access to Document

Fingerprint

Cite this