Abstraction and refinement in local reasoning
File(s)
Accepted version
Author(s)
Dinsdale-Young, T
Gardner, PA
Wheelhouse, M
Type
Conference Paper
Abstract
Local reasoning has become a well-established technique in program verification, which has been shown to be useful at many different levels of abstraction. In separation logic, we use a low-level abstraction that is close to how the machine sees the program state. In context logic, we work with high-level abstractions that are close to how the clients of modules see the program state.We apply program refinement to local reasoning, demonstrating that high-level local reasoning is sound for module implementations.We consider two approaches: one that preserves the high-level locality at the low level; and one that breaks the high-level ’fiction’ of locality.
Date Issued
2010-08-16
Date Acceptance
2010-08-16
Citation
Verified Software: Theories, Tools and Experiments, 2010, 6217, pp.199-215
ISBN
978-3-642-15056-2
Publisher
Springer Berlin Heidelberg
Start Page
199
End Page
215
Journal / Book Title
Verified Software: Theories, Tools and Experiments
Volume
6217
Copyright Statement
© 2010 Springer-Verlag Berlin Heidelberg. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-15057-9_14
Identifier
http://www.doc.ic.ac.uk/~pg
Source
VSTTE 2010
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science, Theory & Methods
Computer Science
LOGIC
Artificial Intelligence & Image Processing
08 Information And Computing Sciences
Start Date
2010-08-16
Finish Date
2010-08-19
Coverage Spatial
Edinburgh, UK