Aarhus University Seal / Aarhus Universitets segl

Modular Verification of Linked Lists with Views via Separation Logic

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

We present a separation logic specification and verification of linked lists with views, a data structure from the C5 collection library for .NET. A view is a generalization of the well-known concept of an iterator. Linked lists with views form an interesting case study for verification since they allow mutation through multiple, possibly overlapping, views of the same underlying list. For modularity, we build on a fragment of higher- order separation logic and use abstract predicates to give a specification with respect to which clients can be proved correct. We introduce a novel mathematical model of lists with views, and formulate succinct modular abstract specifications of the operations on the data structure. To show that the concrete implementation realizes the specification, we use frac- tional permissions in a novel way to capture the sharing of data between views and their underlying list. We conclude by suggesting directions for future research that arose from conducting this case study.
Original languageEnglish
JournalJournal of Object Technology
Volume10
Issue1
Pages (from-to)21-40
Number of pages20
ISSN1660-1769
DOIs
Publication statusPublished - Jan 2011
Externally publishedYes

See relations at Aarhus University Citationformats

ID: 73743196