Please use this identifier to cite or link to this item:
Title: The ramifications of sharing in data structures
Authors: Hobor, A. 
Villard, J.
Keywords: aliasing
separation logic
Issue Date: 2013
Citation: Hobor, A.,Villard, J. (2013). The ramifications of sharing in data structures. Conference Record of the Annual ACM Symposium on Principles of Programming Languages : 523-536. ScholarBank@NUS Repository.
Abstract: Programs manipulating mutable data structures with intrinsic sharing present a challenge for modular verification. Deep aliasing inside data structures dramatically complicates reasoning in isolation over parts of these objects because changes to one part of the structure (say, the left child of a dag node) can affect other parts (the right child or some of its descendants) that may point into it. The result is that finding intuitive and compositional proofs of correctness is usually a struggle. We propose a compositional proof system that enables local reasoning in the presence of sharing. While the AI "frame problem" elegantly captures the reasoning required to verify programs without sharing, we contend that natural reasoning about programs with sharing instead requires an answer to a different and more challenging AI problem, the "ramification problem": reasoning about the indirect consequences of actions. Accordingly, we present a RAMIFY proof rule that attacks the ramification problem head-on and show how to reason with it. Our framework is valid in any separation logic and permits sound compositional and local reasoning in the context of both specified and unspecified sharing. We verify the correctness of a number of examples, including programs that manipulate dags, graphs, and overlaid data structures in nontrivial ways. © 2013 ACM.
Source Title: Conference Record of the Annual ACM Symposium on Principles of Programming Languages
ISBN: 9781450318327
ISSN: 07308566
DOI: 10.1145/2429069.2429131
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.