一句话：证明了带 Presburger 算术与数组的符号堆蕴含有效性检查在两个片段中可判定，并给出判定过程。
论文研究分离逻辑中带 Presburger 算术和数组的符号堆蕴含有效性检查问题。第一个结果针对含数组与存在量词的系统：在后续（succedent）中数组大小不被存在量化的条件下，证明判定过程正确；该条件与 Brotherston 等 2017 年提出的条件不同且互不蕴含。核心方法是将符号堆蕴含新颖地翻译为 Presburger 算术公式。第二个结果证明同时含数组与列表的系统可判定，关键技术是把 Berdine 等 2005 年的 unroll collapse 技术扩展到数组、算术以及双链表。
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.Comment: arXiv admin note: text overlap with arXiv:1708.06696
@article{paperbot1314,
title = {Decidability for Entailments of Symbolic Heaps with Arrays},
author = {Daisuke Kimura and Makoto Tatsuta},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 2},
year = {2021},
doi = {10.23638/lmcs-17(2:15)2021}
}