Publication details

Saarland University Computer Science

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               

Login to edit

Legal notice, Privacy policy