A decision procedure for satisfiability in separation logic with inductive predicates

Nikos Gorogiannis

Separation logic, a logic for reasoning about pointers and heap manipulation, has been successfully employed in tools that work with code bases of large sizes. Central to its ability to describe useful specifications are inductive definitions: e.g., linked lists are usually defined in a recursive way. We show that satisfiability for the ``symbolic heap'' fragment of separation logic with general inductively defined predicates is decidable. Our decision procedure is based on the computation of a certain fixed point from the definition of an inductive predicate, called its ``base'', that exactly characterises its satisfiability. Further, we show that the problem is EXPTIME-complete and that our algorithm runs in exponential time. In addition, it becomes NP-complete when the maximum arity over all predicates is bounded by a constant. Finally, we provide an implementation of our decision procedure, and analyse its performance both on a synthetically generated set of test formulas, and on a second test set harvested from the separation logic literature. For the large majority of these test cases, our tool reports times in the low milliseconds.