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 large-scale 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.

  • 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