Publication details

Saarland University Computer Science

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               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009