Verification of Snapshotable Trees using Access Permissions and Typestate

Hannes Mehnert, Jonathan Aldrich

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

    Abstrakt

    We use access permissions and typestate to specify and ver- ify a Java library that implements snapshotable search trees, as well as some client code. We formalize our approach in the Plural tool, a sound modular typestate checking tool. We describe the challenges to verify- ing snapshotable trees in Plural, give an abstract interface specification against which we verify the client code, provide a concrete specification for an implementation and describe proof patterns we found. We also relate this verification approach to other techniques used to verify this data structure.
    OriginalsprogEngelsk
    BogserieLecture Notes in Computer Science
    Vol/bind7304
    Sider (fra-til)187-201
    Antal sider15
    ISSN0302-9743
    DOI
    StatusUdgivet - 2012

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'Verification of Snapshotable Trees using Access Permissions and Typestate'. Sammen danner de et unikt fingeraftryk.

    Citationsformater