Abstraction and Refinement for Local Reasoning
Venue
Proceedings of the 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE’10), pp. 199–215
Publication Year
2010
Identifiers
Authors
- Thomas Dinsdale-Young
- Philippa Gardner
- Mark J. Wheelhouse
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.