A simple model of separation logic for higher-order store

Birkedal, Lars, Reus, Bernhard, Schwinghammer, Jan and Yang, Hongseok (2008) A simple model of separation logic for higher-order store. In: 35th International Colloquium on Automata, Languages and Programming, Keykjavik, ICELAND, JUL 07-11, 2008.

Full text not available from this repository.

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.

Item Type: Conference or Workshop Item (Paper)
Additional Information: Source: AUTOMATA, LANGUAGES AND PROGRAMMING, PT 2, PROCEEDINGS
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Bernhard Reus
Date Deposited: 06 Feb 2012 18:17
Last Modified: 26 Mar 2012 14:16
URI: http://sro.sussex.ac.uk/id/eprint/15640
📧 Request an update