Toggle Main Menu Toggle Search

Open Access padlockePrints

Reasoning about Separation Using Abstraction and Reification

Lookup NU author(s): Professor Cliff JonesORCiD, Dr Nisansala Yatapanage

Downloads

Full text for this publication is not currently held within this repository. Alternative links are provided below where available.


Abstract

Showing that concurrent threads operate on separate portions of their shared state is a way of establishing non-interference. Furthermore, in many useful programs, ownership of parts of the state are exchanged dynamically. Reasoning about separation and ownership of heap-based variables is often conducted using some form of separation logic. This paper examines the issue of separation and investigates the use of abstraction to specify and to reason about separation in program design. Two case studies demonstrate that using separation as an abstraction is a potentially useful approach.


Publication metadata

Author(s): Jones CB, Yatapanage N

Editor(s): Radu Calinescu, Bernhard Rumpe

Publication type: Conference Proceedings (inc. Abstract)

Publication status: Published

Conference Name: 13th International Conference on Software Engineering and Formal Methods (SEFM 2015)

Year of Conference: 2015

Pages: 3-19

Online publication date: 21/08/2015

Acceptance date: 01/01/1900

ISSN: 0302-9743

Publisher: Springer

URL: https://doi.org/10.1007/978-3-319-22969-0_1

DOI: 10.1007/978-3-319-22969-0_1

Library holdings: Search Newcastle University Library for this item

Series Title: Lecture Notes in Computer Science

ISBN: 9783319229683


Share