A Simple Model of Separation Logic for Higher-order Store

Lars Birkedal; Bernhard Reus; Jan Schwinghammer; Hongseok Yang

Publication details

Programming Systems

A Simple Model of Separation Logic for Higher-order Store

Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Hongseok Yang

Int. Conference Automata Logic and Programming (ICALP'08), Vol. 5126 of LNCS, pp. 348--360, Springer, July 2008

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.

Download PDF Show BibTeX

@INPROCEEDINGS{Birkedal:Reus:Schwinghammer:Yang:08,
  title = {A Simple Model of Separation Logic for Higher-order Store},
  author = {Lars Birkedal and Bernhard Reus and Jan Schwinghammer and Hongseok Yang},
  year = {2008},
  month = {Jul},
  publisher = {{Springer}},
  booktitle = {Int. Conference Automata Logic and Programming (ICALP'08)},
  series = {{LNCS}},
  volume = {5126},
  pages = {{348--360}},
}

Legal notice, Privacy policy