|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
The Ramifications of Sharing in Data Structures
If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.
This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending
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. This talk will be illustrated by proofs of examples manipulating dags, graphs, and overlaid data structures.
This talk is part of the Microsoft Research Cambridge, public talks series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsSecond Language Education Group Talk by Gary Dymski: The Neoclassical Sink and the Heterodox Spiral: Why the Twin Global Crisis has not Transformed Economics Cambridge-INET Institute, Faculty of Economics
Other talksDesign of microstructures for enhanced magnetostriction in active composites False Flags, True Lies: Science and Recycled Photography in Conspiracy Theories after 9/11 ‘“Rivers of Blood”: Illustrating Violence and Virtue in Russia’s Early Modern Empire Production Processes Group Seminar - "Generation of biocompatible and stable microparticles from the breakup of high viscosity alginate jets" Unconventional Superconductivity in Quantum-Dot Systems Nanomagnetism: from green computing to cancer therapy