A relational model for confined separation logic

A relational model for confined separation logic (link)
Shuling Wang, L. S. Barbosa and J. N. Oliveira. TASE'08, 2nd IFIP/IEEE Symp. on Theoretical Aspects of Software Engineering, IEEE Computer Society Press, pp 263-270, 2008.

Abstract

Confined separation logic is a new extension to separation logic designed to deal with problems involving dangling references within shared mutable structures. In particular, 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.