A separation logic for sequences in pointer programs and its decidability

TL;DR

This paper introduces sequence-heap separation logic to formalize properties of variable-length sequences in pointer programs, establishing decidability results for certain logical fragments.

Contribution

It proposes a novel logic integrating sequences into separation logic and analyzes the decidability of its fragments, advancing formal reasoning on sequence-manipulating programs.

Findings

Propositional fragment of the logic is decidable.

Fragment with 2 alternations on program variables is undecidable.

Boundaries between decidable and undecidable fragments are characterized.

Abstract

Separation logic and its variants can describe various properties on pointer programs. However, when it comes to properties on sequences, one may find it hard to formalize. To deal with properties on variable-length sequences and multilevel data structures, we propose sequence-heap separation logic which integrates sequences into logical reasoning on heap-manipulated programs. Quantifiers over sequence variables and singleton heap storing sequence (sequence singleton heap) are new members in our logic. Further, we study the satisfiability problem of two fragments. The propositional fragment of sequence-heap separation logic is decidable, and the fragment with 2 alternations on program variables and 1 alternation on sequence variables is undecidable. In addition, we explore boundaries between decidable and undecidable fragments of the logic with prenex normal form.