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

Expand abstract

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