Variables as resources in separation logic.

Article


Bornat, R., Calcagno, C. and Yang, H. 2006. Variables as resources in separation logic. 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), Birmingham, UK. Proceedings in Electronic Notes in Theoretical Computer Science. Elsevier B.V.. 155, pp. 247-276. https://doi.org/10.1016/j.entcs.2005.11.059
TypeArticle
TitleVariables as resources in separation logic.
AuthorsBornat, R., Calcagno, C. and Yang, H.
Abstract

This paper applied the separation logic notions of ownership and permission to ‘stack' variables that made it possible to banish the variable-use side conditions (e.g. on concurrency and frame rules) which bedevil proof in Hoare logic. The paper contained a formal proof system and some example proofs, together with a suggested model.
This work has so far been useful to the small community that is building automated reasoning tools based on separation logic. Its ideas are essential to Parkinson and Vafeiadis' recent treatment of rely/guarantee and separation logic, and to Parkinson's proof of the concurrent stack.

Research GroupFoundations of Computing group
LanguageEnglish
PublisherElsevier B. V.
Journal21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), Birmingham, UK. Proceedings in Electronic Notes in Theoretical Computer Science. Elsevier B.V.
ISSN1571-0661
Publication dates
Print12 May 2006
Publication process dates
Deposited13 Oct 2008
Output statusPublished
Digital Object Identifier (DOI)https://doi.org/10.1016/j.entcs.2005.11.059
Permalink -

https://repository.mdx.ac.uk/item/80qz7

  • 29
    total views
  • 0
    total downloads
  • 1
    views this month
  • 0
    downloads this month

Export as