Graph-Based Approaches to Reasoning in Separation Logic

ABSTRACT

Separation Logic is an extension of Hoare logic that is particularly suitable for reasoning about imperative programs which manipulate heap data structures. It was introduced by Reynolds, O'Hearn, Yang and Ishtiaq about ten years ago and has since been successfully employed in tools that can discover bugs in low-level systems code in an automated fashion.

In the first half of my talk, I will give an accessible short introduction to key concepts found in Separation Logic and the decision problems typically encountered. In the second half, I will talk about some more recent work on graph-based algorithms for entailment checking in a decidable fragment of Separation Logic with pointers and linked lists. This problem was known to be decidale in coNP, however an approach in which Separation Logic formulas are represented as directed graphs can give a polynomial-time decision procedure. I will present the concrete entailment algorithm as well as key underlying ideas and observations that led to this algorithm. Finally, I will conclude with an experimental evaluation of the algorithm which shows that it outperforms state-of-the-art reasoners by orders of magnitudes.

The topics presented in the second half of the talk are based on joint work with Byron Cook (UCL/MSR Cambridge), Samin Ishtiaq (MSR Cambridge), Joel Ouaknine (Oxford), Matthew Parkinson (MSR Cambridge) and James Worrell (Oxford).