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 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 -complete, while quantifier-free entailment becomes -complete and quantified entailment becomes -complete (where 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.
CITATION STYLE
Brotherston, J., & Kanovich, M. (2018). On the Complexity of Pointer Arithmetic in Separation Logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11275 LNCS, pp. 329–349). Springer Verlag. https://doi.org/10.1007/978-3-030-02768-1_18
Mendeley helps you to discover research relevant for your work.