Tractable reasoning in a fragment of separation logic

Conference item

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 paper, we show that the problem can actually be solved in polynomial time. To this end, we represent separation logic formulae as graphs and show 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. We also discuss natural syntactic extensions that render entailment intractable. © 2011 Springer-Verlag.

Authors: Cook, B; Haase, C; Ouaknine, J; Parkinson, M; Worrell, J

• Host title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
• Volume: 6901 LNCS
• Pages: 235-249
• Publication date: 2011-01-01
• DOI: 10.1007/978-3-642-23217-6_16
• EISSN: 1611-3349
• ISSN: 0302-9743
• ISBN: 9783642232169