2018/03/08 by J G. Brotherston, Brotherston, James, Max Kanovich +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1803.03164
openalex publication_date 2018/03/08 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study extensions of the points-to fragment of symbolic-heap separation logic with various forms of Presburger arithmetic constraints. Most significantly, we find that, even in the minimal case when we allow only conjunctions of simple "difference constraints" (x'≤ x+k) where k is an integer, polynomial-time decidability is already impossible: satisfiability becomes NP-complete, while quantifier-free entailment becomes coNP-complete and quantified entailment becomes P2-complete (P2 is the second class in the polynomial-time hierarchy) In fact we prove that the upper bound is the same, P2, even for the full pointer arithmetic but with a fixed pointer offset, where we allow any Boolean combinations of the elementary formulas (x'=x+k0), (x'≤ x+k0), and (x'