# Publication details

##
Permutation Semantics of Separation Logic

Murat Baktiev

Master's Thesis, Saarland University, December 2006

Separation logic is a recent extension of Hoare logic, developed by O'Hearn, Reynolds
and others, where the separation conjunction p*q describes a disjoint partition of the
heap. With this connective, a frame rule can be stated that facilitates local reasoning
about programs using shared mutable data structures in the heap.
Originally, soundness of the logic was proved with respect to a non-deterministic
memory allocation model. However, in some contexts, this artificial non-determinism
interferes with other language features. I develop an alternative semantics of separation
logic, based on deterministic memory allocation.

*Master's Thesis,
Saarland University, 2006*

Download PDF
Show BibTeX

@MASTERSTHESIS{baktiev2006,
title = {Permutation Semantics of Separation Logic},
author = {Murat Baktiev},
year = {2006},
month = {December},
school = {{Saarland University}},
}

Login to edit

Webmaster,
Wed Sep 16 10:47:00 2009