Decidability for Entailments of Symbolic Heaps with Arrays

TL;DR

This paper establishes decidability results for entailments in separation logic with arrays, Presburger arithmetic, and lists, by developing novel translation techniques and extending existing unroll collapse methods.

Contribution

It introduces new decidability results for symbolic heap entailments involving arrays and lists, with specific conditions on array sizes and novel translation approaches.

Findings

Decidability for symbolic heaps with arrays and existential quantifiers under certain conditions.

Decidability for systems combining arrays and lists using extended unroll collapse techniques.

A novel translation from symbolic heap entailments to Presburger arithmetic.

Abstract

This paper presents two decidability results on the validity checking problem for entailments of symbolic heaps in separation logic with Presburger arithmetic and arrays. The first result is for a system with arrays and existential quantifiers. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially quantified. This condition is different from that proposed by Brotherston et al. in 2017 and one of them does not imply the other. The main idea is a novel translation from an entailment of symbolic heaps into a formula in Presburger arithmetic. The second result is the decidability for a system with both arrays and lists. The key idea is to extend the unroll collapse technique proposed by Berdine et al. in 2005 to arrays and arithmetic as well as double-linked lists.