UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

On the Complexity of Pointer Arithmetic in Separation Logic

Brotherston, J; Kanovich, M; (2018) On the Complexity of Pointer Arithmetic in Separation Logic. In: Programming Languages and Systems. (pp. pp. 329-349). Springer: Cham, Switzerland. Green open access

[thumbnail of pointer_arith_SL_APLAS_final.pdf]
Preview
Text
pointer_arith_SL_APLAS_final.pdf - Published version

Download (428kB) | Preview

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 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.

Type: Proceedings paper
Title: On the Complexity of Pointer Arithmetic in Separation Logic
Event: APLAS 2018: Asian Symposium on Programming Languages and Systems
ISBN-13: 9783030027674
Open access status: An open access version is available from UCL Discovery
DOI: 10.1007/978-3-030-02768-1_18
Publisher version: https://doi.org/10.1007/978-3-030-02768-1_18
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
Keywords: Separation logic, Pointer arithmetic, Complexity
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10074307
Downloads since deposit
61Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item