符号堆中带有数组的蕴涵的可判定性
摘要：分离逻辑中带Presburger算术和数组的符号堆的包含有效性检查问题的两个可判定性结果 带有数组和存在量词的系统的第一个结果。在结论中的数组的大小不是存在量词的条件下，决策过程的正确性被证明。这个条件不同于Brotherston等人在2017年提出的条件，其中一个并不蕴含另一个。主要思想是将符号堆的包含转化为Presburger算术中的一个公式。第二个结果是具有数组和列表的系统的可判定性。关键思想是将Berdine等人在2005年提出的unroll collapse技术扩展到数组、算术和双向链表。
作者：Daisuke Kimura and Makoto Tatsuta
论文ID：1802.05935
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22