<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>47</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">S. Wang</style></author><author><style face="normal" font="default" size="100%">Luis Soares Barbosa</style></author><author><style face="normal" font="default" size="100%">José Nuno Oliveira</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">A relational model for confined separation logic</style></title><secondary-title><style face="normal" font="default" size="100%">2nd IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering - TASE</style></secondary-title></titles><dates><year><style  face="normal" font="default" size="100%">2008</style></year><pub-dates><date><style  face="normal" font="default" size="100%">June</style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/lsb/files/tase08-wbo.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">IEEE Computer Society</style></publisher><pub-location><style face="normal" font="default" size="100%">Nanjing, China</style></pub-location><pages><style face="normal" font="default" size="100%">263-270</style></pages><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;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.&lt;/p&gt;
</style></abstract></record></records></xml>