A Proof System for Separation Logic with Magic Wand
Wonyeol Lee, Jineon Baek, and Sungwoo Park
Introduction
Separation logic is an extension of Hoare logic
which is acknowledged as an enabling technology for largescale program verification.
It features two new logical connectives,
separating conjunction and separating implication,
but most of the applications of separation logic have exploited
only separating conjunction without considering separating implication.
Nevertheless the power of separating implication has been well recognized
and there is a growing interest in its use for program verification.
We develop a proof system P_SL for full separation logic
which supports not only separating conjunction but also separating implication.
The proof system P_SL is developed in the style of sequent calculus and satisfies the admissibility of cut.
The key challenge in the development of P_SL is to devise a set of inference rules for manipulating heap structures
that ensure its completeness with respect to separation logic.
We show that our proof of completeness directly translates to a proof search strategy.

A Proof System for Separation Logic with Magic Wand.
Wonyeol Lee and Sungwoo Park.
POPL 2014.
[PDF]

A Proof System for Separation Logic with Magic Wand.
Wonyeol Lee and Sungwoo Park.
Technical Report POSTECHCSE20137, Pohang University of Science and Technology (POSTECH), July 2013.
[PDF]

A Proof System for Separation Logic with Magic Wand.
Wonyeol Lee, Jineon Baek, and Sungwoo Park.
Submitted for publication, April 2015.
[PDF]
[PDF (with all proofs)]
UPDATE [2014.1.18] The rule Disj* in P_SL is unsound in the original semantics of separation logic.
It gives rise to another interpretation of formulas of separation logic that is incompatible with the original semantics of separation logic.
UPDATE [2014.1.19] By removing the rule Disj* from the proof system P_SL, we obtain a proof system
that is sound but incomplete with respect to the original semantics of separation logic.
That is, the semantics for separation logic assumed in P_SL is sound but incomplete with respect to the original semantics of separation logic
while P_SL (without the rule Disj*) is sound and complete with respect to our semantics for separation logic.
We can also obtain a proof search strategy that is sound but incomplete with respect to P_SL.
Email us at .
Programming Language Laboratory
Department of Computer Science and Engineering
Pohang University of Science and Technology (POSTECH)
Republic of Korea