##
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.