Modular verification of a non-blocking stack.

Article

Bornat, R., Parkinson, M. and O'Hearn, P. 2007. Modular verification of a non-blocking stack. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '07), Nice, France. Proceedings.. https://doi.org/10.1145/1190216.1190261
TypeArticle
TitleModular verification of a non-blocking stack.
AuthorsBornat, R., Parkinson, M. and O'Hearn, P.
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
PublisherAssociation for Computing Machinery (ACM)
Journal34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '07), Nice, France. Proceedings.
ISSN0362-1340
Publication dates
Print17 Jan 2007
Publication process dates
Deposited13 Oct 2008
Output statusPublished
Digital Object Identifier (DOI)https://doi.org/10.1145/1190216.1190261
LanguageEnglish
Page range297-302
Permalink -

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

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

Export as