Abstraction and Refinement for Local Reasoning

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.

Venue

Proceedings of the 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE’10), pp. 199–215

Publication Date

2010

Identifiers

Source Materials