带数组的符号堆蕴含判定过程
计算机科学中的逻辑
2017-08-29 v2
摘要
本文给出了一个判定过程，用于判定在包含 Presburger 算术和数组的分离逻辑中符号堆蕴含的有效性。在后继式中数组大小不受存在量词约束的条件下，证明了该判定过程的正确性。该条件独立于 Brotherston 等人在 CADE-2017 论文中提出的条件，即二者互不蕴含。为提高判定过程的效率，本文还提出了一些技术。该判定过程的主要思想是将符号堆的蕴含新颖地转化为 Presburger 算术中的公式，并将其与外部 SMT 求解器结合。本文还给出了实现的实验结果，表明该判定过程的效率足以投入实际使用。
引用
@article{arxiv.1708.06696,
title = {Decision Procedure for Entailment of Symbolic Heaps with Arrays},
author = {Daisuke Kimura and Makoto Tatsuta},
journal= {arXiv preprint arXiv:1708.06696},
year = {2017}
}