Modular verification of linked lists with views via separation logic

Jonas Braband Jensen, Lars Birkedal, Peter Sestoft

    Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

    Abstract

    We present a separation logic specification and verification of linked lists with views, a data structure from the C5 collection library for C#. 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 of multiple possibly-overlapping views of the same underlying list. For modularity, we present our specification in 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 fractional 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.
    Translated title of the contributionModulær verifikation af "linked lists with views" via separationslogik
    Original languageEnglish
    Title of host publicationProceedings of the 12th Workshop on Formal Techniques for Java-Like Programs
    Number of pages7
    Place of PublicationNew York, NY, USA
    PublisherAssociation for Computing Machinery
    Publication date31 Dec 2010
    Pages4:1--4:7
    ISBN (Electronic)978-1-4503-0540-2
    DOIs
    Publication statusPublished - 31 Dec 2010

    Keywords

    • Separation Logic
    • Linked Lists
    • Views
    • Modular Verification
    • Fractional Permissions

    Cite this