A Simple Model of Separation Logic for Higher-order Store

Lars Birkedal; Bernhard Reus; Jan Schwinghammer; Hongseok Yang

A Simple Model of Separation Logic for Higher-order Store

Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Hongseok Yang

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

Abstract

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 language	English
Book series	Lecture Notes in Computer Science
Pages (from-to)	348-360
ISSN	0302-9743
Publication status	Published - 2008
Event	ICALP 2008 35th International Colloquium on Automata, Languages and Programming - Reykjavik, Iceland Duration: 6 Jul 2008 → 13 Jul 2008 Conference number: 35

Conference

Conference	ICALP 2008 35th International Colloquium on Automata, Languages and Programming
Number	35
Country/Territory	Iceland
City	Reykjavik
Period	06/07/2008 → 13/07/2008

Keywords

Separation Logic
Pointer-Manipulating Programs
Higher-Order Store
Semantics
Specification Logic

Cite this

@inproceedings{9ebf89f0832e11ddb75b000ea68e967b,

title = "A Simple Model of Separation Logic for Higher-order Store",

abstract = "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.",

keywords = "Separation Logic, Pointer-Manipulating Programs, Higher-Order Store, Semantics, Specification Logic, Separation Logic, Pointer-Manipulating Programs, Higher-Order Store, Semantics, Specification Logic",

author = "Lars Birkedal and Bernhard Reus and Jan Schwinghammer and Hongseok Yang",

note = "Serie: Lecture Notes in Computer Science, Springer, 0302-9743, 1611-3349 Volumne: 5126/2008; ICALP 2008 35th International Colloquium on Automata, Languages and Programming ; Conference date: 06-07-2008 Through 13-07-2008",

year = "2008",

language = "English",

pages = "348--360",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer",

}

TY - GEN

T1 - A Simple Model of Separation Logic for Higher-order Store

AU - Birkedal, Lars

AU - Reus, Bernhard

AU - Schwinghammer, Jan

AU - Yang, Hongseok

N1 - Conference code: 35

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

KW - Separation Logic

KW - Pointer-Manipulating Programs

KW - Higher-Order Store

KW - Semantics

KW - Specification Logic

KW - Separation Logic

KW - Pointer-Manipulating Programs

KW - Higher-Order Store

KW - Semantics

KW - Specification Logic

M3 - Conference article

SN - 0302-9743

SP - 348

EP - 360

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - ICALP 2008 35th International Colloquium on Automata, Languages and Programming

Y2 - 6 July 2008 through 13 July 2008

ER -