FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
On the Complexity of Pointer Arithmetic in Separation Logic

Authors: James Brotherston and Max Kanovich

Paper Information

Title:On the Complexity of Pointer Arithmetic in Separation Logic
Authors:James Brotherston and Max Kanovich
Proceedings:ADSL Papers
Editor: Nikos Gorogiannis
Keywords:separation logic, pointer arithmetic, complexity
Abstract:

ABSTRACT. 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 \Pi^P_2-complete (where \Pi^P_2 is the second class in the polynomial-time hierarchy).

However, the language does satisfy the small model property, meaning that any satisfiable formula A has a model of size polynomial in A, whereas this property fails when richer forms of arithmetical constraints are permitted.

Pages:18
Talk:Jul 13 14:50 (Session 87B: Weak Memory and Complexity)
Paper: