A Proof System for Separation Logic with Magic Wand
SCIE
SCOPUS
- Title
- A Proof System for Separation Logic with Magic Wand
- Authors
- Lee, W; Park, S
- Date Issued
- 2014-01
- Publisher
- ACM
- Abstract
- 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. This paper develops a proof system for full separation logic which supports not only separating conjunction but also separating implication. The proof system is developed in the style of sequent calculus and satisfies the admissibility of cut. The key challenge in the development is to devise a set of inference rules for manipulating heap structures that ensure the completeness of the proof system with respect to separation logic. We show that our proof of completeness directly translates to a proof search strategy.
- Keywords
- Verification; Separation logic; Proof system; Theorem prover; MUTABLE DATA-STRUCTURES; SHAPE-ANALYSIS; VERIFICATION; BI
- URI
- https://oasis.postech.ac.kr/handle/2014.oak/14755
- DOI
- 10.1145/2535838.2535871
- ISSN
- 0362-1340
- Article Type
- Article
- Citation
- SIGPLAN Notices, vol. 49, no. 1, page. 477 - 490, 2014-01
- Files in This Item:
- There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.