Daisuke Kimura ; Makoto Tatsuta - Decidability for Entailments of Symbolic Heaps with Arrays

lmcs:4294 - Logical Methods in Computer Science, May 11, 2021, Volume 17, Issue 2 - https://doi.org/10.23638/LMCS-17(2:15)2021
Decidability for Entailments of Symbolic Heaps with ArraysArticle

Authors: Daisuke Kimura ; Makoto Tatsuta

    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.


    Volume: Volume 17, Issue 2
    Published on: May 11, 2021
    Accepted on: January 4, 2021
    Submitted on: February 19, 2018
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1509 times.
    This article's PDF has been downloaded 270 times.