带数组的符号堆蕴涵的可判定性
计算机科学中的逻辑
2023-06-22 v4
摘要
本文给出了关于带普雷斯伯格算术与数组的分离逻辑中符号堆蕴涵有效性检查问题的两个可判定性结果。第一个结果针对带数组与存在量词的系统。该判定过程的正确性在后续项（succedent）中数组大小不被存在量词约束的条件下得到证明。此条件不同于Brotherston等人于2017年提出的条件，且二者互不蕴含。主要思想是将符号堆的蕴涵新颖地翻译为普雷斯伯格算术中的公式。第二个结果是带数组与列表系统的可判定性。关键思想是将Berdine等人于2005年提出的展开折叠技术推广到数组、算术以及双链表。
引用
@article{arxiv.1802.05935,
title = {Decidability for Entailments of Symbolic Heaps with Arrays},
author = {Daisuke Kimura and Makoto Tatsuta},
journal= {arXiv preprint arXiv:1802.05935},
year = {2023}
}
备注
arXiv admin note: text overlap with arXiv:1708.06696