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.
|Bogserie||Lecture Notes in Computer Science|
|Status||Udgivet - 2008|
|Begivenhed||ICALP 2008 35th International Colloquium on Automata, Languages and Programming - Reykjavik, Island|
Varighed: 6 jul. 2008 → 13 jul. 2008
Konferencens nummer: 35
|Konference||ICALP 2008 35th International Colloquium on Automata, Languages and Programming|
|Periode||06/07/2008 → 13/07/2008|