University of Sussex
Browse

File(s) not publicly available

A simple model of separation logic for higher-order store

presentation
posted on 2023-06-07, 19:30 authored by Lars Birkedal, Bernhard ReusBernhard Reus, Jan Schwinghammer, Hongseok Yang
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.

History

Publication status

  • Published

ISSN

0302-9743

Publisher

SPRINGER-VERLAG BERLIN, HEIDELBERGER PLATZ 3, D-14197 BERLIN, GERMANY

Volume

5126

Page range

348-360

Presentation Type

  • paper

Event name

35th International Colloquium on Automata, Languages and Programming

Event location

Keykjavik, ICELAND, JUL 07-11, 2008

Event type

conference

ISBN

978-3-540-70582-6

Department affiliated with

  • Informatics Publications

Notes

Source: AUTOMATA, LANGUAGES AND PROGRAMMING, PT 2, PROCEEDINGS

Full text available

  • No

Peer reviewed?

  • Yes

Legacy Posted Date

2012-02-06

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC