A Simple Model of Separation Logic for Higher-order Store

Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Hongseok Yang

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftKonferenceartikelForskningpeer review

    Abstrakt

    Separation logic is a Hoare-style logic for reasoning about pointer-manipulating programs. Its core ideas have recently been extended from low-level to richer, high-level languages. In this paper we develop a new semantics of the logic for a programming language where code can be stored (i.e., with higher-order store). The main improvement on previous work is the simplicity of the model. As a consequence, several restrictions imposed by the semantics are removed, leading to a considerably more natural assertion language with a powerful specification logic.
    OriginalsprogEngelsk
    BogserieLecture Notes in Computer Science
    Sider (fra-til)348-360
    ISSN0302-9743
    StatusUdgivet - 2008
    BegivenhedICALP 2008 35th International Colloquium on Automata, Languages and Programming - Reykjavik, Island
    Varighed: 6 jul. 200813 jul. 2008
    Konferencens nummer: 35

    Konference

    KonferenceICALP 2008 35th International Colloquium on Automata, Languages and Programming
    Nummer35
    Land/OmrådeIsland
    ByReykjavik
    Periode06/07/200813/07/2008

    Citationsformater