带数组的符号堆蕴含式的可判定性
Decidability for Entailments of Symbolic Heaps with Arrays
AI总结：
本文证明了分离逻辑中带数组的符号堆蕴含式的两个可判定性结果，分别针对带存在量词的系统（在特定条件下）和同时带数组与列表的系统，核心方法包括转换为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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
