Book chapter
On the Complexity of Pointer Arithmetic in Separation Logic.
We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study an extension of the points-to fragment of symbolic-heap separation logic with sets of simple “difference constraints” of the form x≤y+k
, where x and y are pointer variables and k is an integer offset. This extension can be considered a practically minimal language for separation logic with pointer arithmetic.
Most significantly, we find that, even for this minimal language, polynomial-time decidability is already impossible: satisfiability becomes NP
-complete, while quantifier-free entailment becomes coNP-complete and quantified entailment becomes ΠP2-complete (where ΠP2
is the second class in the polynomial-time hierarchy).
However, the language does satisfy the small model property, meaning that any satisfiable formula has a model, and any invalid entailment has a countermodel, of polynomial size, whereas this property fails when richer forms of arithmetical constraints are permitted.