Variables as resource in Hoare logic.

Book chapter

Bornat, R., Calcagno, C. and Parkinson, M. 2006. Variables as resource in Hoare logic. in: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), Seattle, Washington. Proceedings. IEEE Computer Society. pp. 137-146
Chapter titleVariables as resource in Hoare logic.
AuthorsBornat, R., Calcagno, C. and Parkinson, M.
Abstract

This paper contains a model and a proof of soundness for a range of program logics based on separation logic and including the notions of permission and ownership for stack variables. It shows that there is no loss of expressive power (all proofs in Hoare logic are expressible). This permits the construction of program-reasoning tools that use the notion of ‘variables as resource'.
This is a highly technical piece of work, and its impact will emerge when more tools have been constructed. Variables-as-resource will be necessary if such tools are to emerge.

Research GroupFoundations of Computing group
Page range137-146
Book title21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), Seattle, Washington. Proceedings.
PublisherIEEE Computer Society
ISBN
Hardcover0-7695-2631-4
ISSN0-7695-2631-4
Publication dates
Print01 Aug 2006
Publication process dates
Deposited13 Oct 2008
Output statusPublished
Web address (URL)http://ieeexplore.ieee.org/search/wrapper.jsp?arnumber=1691225
Digital Object Identifier (DOI)https://doi.org/10.1109/LICS.2006.52
LanguageEnglish
Journal21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), Seattle, Washington. Proceedings, IEEE Computer Society.
Permalink -

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

Log in to edit
  • 32
    total views
  • 0
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as