Local Action and Abstract Separation Logic

tion and Abstract Separation Logic Cristiano Calcagno Imperial College, London 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 separaebras, 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.

• Type: Conference
• Year: 2007
• Where: LICS
• Authors: Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang
• Keywords: Computer Science, LICS 2007, Local Actions, Separation Logic, Separation Logic Cristiano