The Ramification Rule of Separation Logic

Presented as part of the 2012 HCSS conference.

Abstract:

Separation logic provided a breakthrough in reasoning about the heap in many cases, making specs and proofs tractable and close to the programmer's intuition. Its "frame rule" enables local reasoning by answering the frame problem: describing what does not change when updating parts of the heap. However, for algorithms exhibiting intrinsic sharing, neither separation logic nor any other formalism has achieved simple proofs. We propose that most programs manipulating graphs, DAGs, or overlaid data structures require an answer to a different problem, the ramification problem (like the frame problem, another classic AI problem): describing how global structures change because of a local update. This work presents a solution in the form of a new inference rule: the ramification rule, mixing separation logic and relevant logic, and valid in any separation logic. We show how it allows sound and local reasoning about effects on data structures with sharing.

Biography:

Jules Villard is a research assistant working in the Programming Principles, Logic, and Verification group led by Peter O'Hearn at University College London (UK). He has worked on compositional techniques for the verification of message-passing programs, as highlighted by his PhD thesis (2011). He is the creator of the Heap-Hop academic prototype, capable of specifying and verifying message-passing programs operating over a shared memory. His current research involves the areas of program verification, compositional reasoning, and concurrency.