Formalized Verification of Snapshotable Trees: Separation and Sharing

Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, Peter Sestoft

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

Abstrakt

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.

OriginalsprogEngelsk
TitelVerified Software: Theories, Tools, Experiments : 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings
Antal sider15
Vol/bind 7152
ForlagSpringer
Publikationsdato2012
Sider179-195
ISBN (Trykt)978-3-642-27704-7
DOI
StatusUdgivet - 2012
NavnLecture Notes in Computer Science
Vol/bind7152
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'Formalized Verification of Snapshotable Trees: Separation and Sharing'. Sammen danner de et unikt fingeraftryk.

Citationsformater