Deciding Entailment in SL with Possibly-empty Lists is Polytime

Christoph Haase

In 2004, Berdine, Calcagno and O'Hearn introduced a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. They showed that entailment in this fragment is in coNP, but the precise complexity of this problem has been open since. In this talk, I am going to show that the problem can actually be solved in polynomial time. To this end, separation logic formulae are represented as graphs and it is shown that every satisfiable formula is equivalent to one whose graph is in a particular normal form. Entailment between two such formulae then reduces to a graph homomorphism problem. Furthermore, I am going to discuss natural syntactic extensions that render entailment intractable.

Work in progress with Byron Cook, Joel Ouaknine, Matthew Parkinson and James Worrell.