Aarhus University Seal / Aarhus Universitets segl

Formalized verification of snapshotable trees: Separation and sharing

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

We use separation logic to specify and verify a Java program that implements snapshotable search trees, fully formalizing the specification and verification in the Coq proof assistant. We achieve local and modular reasoning about a tree and its snapshots and their iterators, although 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 implementations and verifies the first one. The others are included as future work and as a set of challenge problems for full functional specification and verification, whether by separation logic or by other formalisms.

Original languageEnglish
Title of host publicationVerified Software: Theories, Tools, Experiments : 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings
EditorsRajeev Joshi, Peter Müller, Andreas Podelski
Number of pages17
PublisherSpringer
Publication year7 Feb 2012
Pages179-195
ISBN (print)9783642277047
ISBN (Electronic)978-3-642-27705-4
DOIs
Publication statusPublished - 7 Feb 2012
Externally publishedYes
SeriesLecture Notes in Computer Science
Volume7152
ISSN0302-9743

See relations at Aarhus University Citationformats

ID: 81390150