A relational model for confined separation logic

Citation:
Wang S, Barbosa LS, Oliveira JN.  2008.  A relational model for confined separation logic. 2nd IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering - TASE. :263-270.

Date Presented:

June

Abstract:

Confined separation logic is a new extension to separation logic designed to deal with problems involving dangling references within shared mutable structures. In par- ticular, it allows for reasoning about confinement in object- oriented programs. In this paper, we discuss the semantics of such an extension by defining a relational model for the overall logic, parametric on the shapes of both the store and the heap. This model provides a simple and elegant interpretation of the new confinement connectives and helps in seeking for duals. A number of properties of this logic are proved calculationally.

Citation Key:

WBO08

DOI:

10.1109/TASE.2008.38

PreviewAttachmentSize
tase08-wbo.pdf307.99 KB