A Simple Model of Separation Logic for Higher-order Store

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperConference articleResearchpeer-review

  • Lars Birkedal
  • Bernhard Reus, United Kingdom
  • Jan Schwinghammer, Germany
  • Hongseok Yang, United Kingdom
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.
Original languageEnglish
Book seriesLecture Notes in Computer Science
Pages (from-to)348-360
ISSN0302-9743
Publication statusPublished - 2008
Externally publishedYes

See relations at Aarhus University Citationformats

ID: 73743565