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