A Relational Model for Confined Separation Logic

摘要：

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.

作者: Shuling Wang L.S.Barbosa J.N.Oliveira

作者单位: LMAM and Department of Informatics School of Mathematical Sciences Peking University, Beijing, China CCTC and Department of Informatics Minho University Portugal

会议类型: 国际会议

会议名称: 第二届IFIP/IEEE软件工程理论基础国际研讨会(TASE 2008)(Second IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering)

会议地点: 南京

会议语种:英文

页码: 263-270

在线出版日期: 2008-06-17（万方平台首次上网日期，不代表论文的发表时间）