loading...
A Relational Model for Confined Separation Logic
June 17-June 19
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2008.382008 2nd IFIP/IEEE International Symp ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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.
Index Terms:
relational, point-free, confined separation logic
Citation:
Shuling Wang, L.S. Barbosa, J.N. Oliveira, "A Relational Model for Confined Separation Logic," tase, pp.263-270, 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 2008
Usage of this product signifies your acceptance of the Terms of Use.