关于符号堆分离逻辑鲁棒性质的统一推理
计算机科学中的逻辑
2016-10-25 v1
摘要
我们引入了堆自动机（heap automata），这是一种用于对用户定义归纳谓词的分离逻辑符号堆片段的鲁棒性质进行自动推理的形式化方法。鲁棒性质（如可满足性、可达性和无环性）对于基于分离逻辑的自动化程序分析和验证中的广泛推理任务至关重要。此前，此类性质出现在分离逻辑文献的许多地方，但尚未以系统的方式进行研究。在本文中，我们开发了一个基于堆自动机的算法框架，使我们能够以统一的方式为广泛的鲁棒性质推导渐近最优的判定过程。我们实现了该框架的原型，并在上述所有鲁棒性质方面获得了令人鼓舞的结果。此外，我们展示了堆自动机在鲁棒性质之外的适用性。我们将算法框架应用于符号堆分离逻辑的模型检测和蕴涵问题。
引用
@article{arxiv.1610.07041,
title = {Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic},
author = {Christina Jansen and Jens Katelaan and Christoph Matheja and Thomas Noll and Florian Zuleger},
journal= {arXiv preprint arXiv:1610.07041},
year = {2016}
}