Two for the Price of One: Lifting Separation Logic Assertions.

Jacob Junker Thamsborg, Lars Birkedal, Hongseok Yang

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

    Abstract

    Recently, data abstraction has been studied in the context of separation logic, with noticeable practical successes: the developed logics have enabled clean proofs of tricky challenging programs, such as subject-observer patterns, and they have become the basis of efficient verification tools for Java (jStar), C (VeriFast) and Hoare Type Theory (Ynot). In this paper, we give a new semantic analysis of such logic-based approaches using Reynolds's relational parametricity. The core of the analysis is our lifting theorems, which give a sound and complete condition for when a true implication between assertions in the standard interpretation entails that the same implication holds in a relational interpretation. Using these theorems, we provide an algorithm for identifying abstraction-respecting client-side proofs; the proofs ensure that clients cannot distinguish two appropriately-related module implementations.
    OriginalsprogEngelsk
    TidsskriftLogical Methods in Computer Science
    Vol/bind8
    Udgave nummer3
    ISSN1860-5974
    StatusUdgivet - 2012

    Emneord

    • Data Abstraction
    • Separation Logic
    • Relational Parametricity
    • Formal Verification
    • Module Implementations

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'Two for the Price of One: Lifting Separation Logic Assertions.'. Sammen danner de et unikt fingeraftryk.

    Citationsformater