Formalized Verification of Snapshotable Trees: Separation and Sharing

Hannes Mehnert; Filip Sieczkowski; Lars Birkedal; Peter Sestoft

doi:10.1007/978-3-642-27705-4_15

Formalized Verification of Snapshotable Trees: Separation and Sharing

Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, Peter Sestoft

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Abstract

We use separation logic to specify and verify a Java program
that implements snapshotable search trees, fully formalizing the speci-
cation and verication in the Coq proof assistant. We achieve local and
modular reasoning about a tree and its snapshots and their iterators, al-
though the implementation involves shared mutable heap data structures
with no separation or ownership relation between the various data.
The paper also introduces a series of four increasingly sophisticated im-
plementations and veries the rst one. The others are included as future
work and as a set of challenge problems for full functional specication
and verication, whether by separation logic or by other formalisms.

Original language	English
Title of host publication	Verified Software: Theories, Tools, Experiments : 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings
Number of pages	15
Volume	7152
Publisher	Springer
Publication date	2012
Pages	179-195
ISBN (Print)	978-3-642-27704-7
DOIs	https://doi.org/10.1007/978-3-642-27705-4_15
Publication status	Published - 2012

Series	Lecture Notes in Computer Science
Volume	7152
ISSN	0302-9743

Keywords

Separation Logic
Snapshotable Search Trees
Coq Proof Assistant
Local and Modular Reasoning
Shared Mutable Heap Data Structures

Access to Document

10.1007/978-3-642-27705-4_15

Formalized Verification of Snapshotable Trees.pdfSubmitted manuscript, 206 KB

ToMeSo: Tools and Methods for Scalable Software Verifications
Sestoft, P. (CoI), Birkedal, L. (PI), Mehnert, H. (CoI), Jensen, J. B. (CoI), Bengtson, J. (CoI), Thamsborg, J. J. (CoI), Hartmann Jensen, M. (CoI), Sieczkowski, F. (CoI), Mehnert, H. (CoI) & Svendsen, K. (CoI)
Independent Research Fund Denmark
01/03/2009 → 30/06/2013
Project: Research

Cite this

@inproceedings{35a9addf75f040d3aab14d3f23e265a1,

title = "Formalized Verification of Snapshotable Trees: Separation and Sharing",

abstract = "We use separation logic to specify and verify a Java program that implements snapshotable search trees, fully formalizing the speci- cation and verication in the Coq proof assistant. We achieve local and modular reasoning about a tree and its snapshots and their iterators, al- though the implementation involves shared mutable heap data structures with no separation or ownership relation between the various data. The paper also introduces a series of four increasingly sophisticated im- plementations and veries the rst one. The others are included as future work and as a set of challenge problems for full functional specication and verication, whether by separation logic or by other formalisms.",

keywords = "Separation Logic, Snapshotable Search Trees, Coq Proof Assistant, Local and Modular Reasoning, Shared Mutable Heap Data Structures, Separation Logic, Snapshotable Search Trees, Coq Proof Assistant, Local and Modular Reasoning, Shared Mutable Heap Data Structures",

author = "Hannes Mehnert and Filip Sieczkowski and Lars Birkedal and Peter Sestoft",

year = "2012",

doi = "10.1007/978-3-642-27705-4_15",

language = "English",

isbn = "978-3-642-27704-7",

volume = " 7152",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "179--195 ",

booktitle = "Verified Software: Theories, Tools, Experiments",

address = "Germany",

}

Mehnert, H, Sieczkowski, F, Birkedal, L & Sestoft, P 2012, Formalized Verification of Snapshotable Trees: Separation and Sharing. in Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings. vol. 7152, Springer, Lecture Notes in Computer Science, vol. 7152, pp. 179-195 . https://doi.org/10.1007/978-3-642-27705-4_15

Formalized Verification of Snapshotable Trees: Separation and Sharing. / Mehnert, Hannes; Sieczkowski, Filip; Birkedal, Lars et al.
Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings. Vol. 7152 Springer, 2012. p. 179-195 (Lecture Notes in Computer Science, Vol. 7152).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Formalized Verification of Snapshotable Trees: Separation and Sharing

AU - Mehnert, Hannes

AU - Sieczkowski, Filip

AU - Birkedal, Lars

AU - Sestoft, Peter

PY - 2012

Y1 - 2012

N2 - We use separation logic to specify and verify a Java program that implements snapshotable search trees, fully formalizing the speci- cation and verication in the Coq proof assistant. We achieve local and modular reasoning about a tree and its snapshots and their iterators, al- though the implementation involves shared mutable heap data structures with no separation or ownership relation between the various data. The paper also introduces a series of four increasingly sophisticated im- plementations and veries the rst one. The others are included as future work and as a set of challenge problems for full functional specication and verication, whether by separation logic or by other formalisms.

AB - We use separation logic to specify and verify a Java program that implements snapshotable search trees, fully formalizing the speci- cation and verication in the Coq proof assistant. We achieve local and modular reasoning about a tree and its snapshots and their iterators, al- though the implementation involves shared mutable heap data structures with no separation or ownership relation between the various data. The paper also introduces a series of four increasingly sophisticated im- plementations and veries the rst one. The others are included as future work and as a set of challenge problems for full functional specication and verication, whether by separation logic or by other formalisms.

KW - Separation Logic

KW - Snapshotable Search Trees

KW - Coq Proof Assistant

KW - Local and Modular Reasoning

KW - Shared Mutable Heap Data Structures

KW - Separation Logic

KW - Snapshotable Search Trees

KW - Coq Proof Assistant

KW - Local and Modular Reasoning

KW - Shared Mutable Heap Data Structures

U2 - 10.1007/978-3-642-27705-4_15

DO - 10.1007/978-3-642-27705-4_15

M3 - Article in proceedings

SN - 978-3-642-27704-7

VL - 7152

T3 - Lecture Notes in Computer Science

SP - 179

EP - 195

BT - Verified Software: Theories, Tools, Experiments

PB - Springer

ER -

Mehnert H, Sieczkowski F, Birkedal L, Sestoft P. Formalized Verification of Snapshotable Trees: Separation and Sharing. In Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings. Vol. 7152. Springer. 2012. p. 179-195 . (Lecture Notes in Computer Science, Vol. 7152). doi: 10.1007/978-3-642-27705-4_15

Formalized Verification of Snapshotable Trees: Separation and Sharing

Abstract

Keywords

Access to Document

Fingerprint

Projects

ToMeSo: Tools and Methods for Scalable Software Verifications

Cite this