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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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.

Originalsprog	Engelsk
Titel	Verified Software: Theories, Tools, Experiments : 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings
Antal sider	15
Vol/bind	7152
Forlag	Springer
Publikationsdato	2012
Sider	179-195
ISBN (Trykt)	978-3-642-27704-7
DOI	https://doi.org/10.1007/978-3-642-27705-4_15
Status	Udgivet - 2012

Navn	Lecture Notes in Computer Science
Vol/bind	7152
ISSN	0302-9743

Emneord

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

Adgang til dokumentet

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

Formalized Verification of Snapshotable Trees.pdfIndsendt manuskript, 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)
Danmarks Frie Forskningsfond
01/03/2009 → 30/06/2013
Projekter: Projekt › Forskning

Citationsformater

@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. i Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings. bind 7152, Springer, Lecture Notes in Computer Science, bind 7152, s. 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. Bind 7152 Springer, 2012. s. 179-195 (Lecture Notes in Computer Science, Bind 7152).

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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. I Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings. Bind 7152. Springer. 2012. s. 179-195 . (Lecture Notes in Computer Science, Bind 7152). doi: 10.1007/978-3-642-27705-4_15

Formalized Verification of Snapshotable Trees: Separation and Sharing

Abstract

Emneord

Adgang til dokumentet

Fingeraftryk

Projekter

ToMeSo: Tools and Methods for Scalable Software Verifications

Citationsformater