loading...
Local Action and Abstract Separation Logic
Wroclaw, Poland July 10-July 14
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2007.3022nd Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Cristiano Calcagno, Imperial College, London, UK
Peter W. O'Hearn, Queen Mary, University of London
Hongseok Yang, Queen Mary, University of London
Separation logic is an extension of Hoare?s logic which supports a local way of reasoning about programs that mutate memory. We present a study of the semantic structures lying behind the logic. The core idea is of a local action, a state transformer that mutates the state in a local way. We formulate local actions for a class of models called separation algebras, abstracting from the RAM and other specific concrete models used in work on separation logic. Local actions provide a semantics for a generalized form of (sequential) separation logic. We also show that our conditions on local actions allow a general soundness proof for a separation logic for concurrency, interpreted over arbitrary separation algebras.
Citation:
Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang, "Local Action and Abstract Separation Logic," lics, pp.366-378, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.