Separation logic and abstraction

Matthew Parkinson, Gavin Bierman
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 15 February 2020

SIGPLAN Not. 40(1)
Association for Computing Machinery
New York, NY, USA
Pages 247-258
January 2005
Topic(s): verification
Note(s): permission logic, separation logic

This paper tackles three problems:

  • Supporting user-defined predicates in separation logic, adding OPEN and CLOSE rules to unfold and fold their definitions.

  • Placing restrictions on where OPEN/CLOSE can be used in order to enforce data abstractions.

  • Generalizing abstract predicates to support object-oriented languages by adding abstract predicate families that can be indexed by the class.

There are a number of examples manually proved in this paper.

  • Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]