Paper: Local Action and Abstract Separation Logic (at LICS 2007)

Authors: Cristiano Calcagno Peter W. O'Hearn Hongseok Yang

Abstract

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.

BibTeX

  @InProceedings{CalcagnoOHearnYang-LocalActionandAbstr,
    author = 	 {Cristiano Calcagno and Peter W. O'Hearn and Hongseok Yang},
    title = 	 {Local Action and Abstract Separation Logic},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {366--375},
    location =   {Wroclaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }