Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
复制标题
符号堆分离逻辑鲁棒性的统一推理
DOI：
10.1007/978-3-662-54434-1_23
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Florian Zuleger
中科院分区：
文献类型：
--
作者：
Christina Jansen;Jens Katelaan;Christoph Matheja;Thomas Noll;Florian Zuleger
我们介绍了堆自动机，自动推理aboutrobustness properties的符号堆片段的分离逻辑与用户定义的归纳谓词的形式主义。可满足性、可达性和非循环性等鲁棒性属性对于基于分离逻辑的自动程序分析和验证中的各种推理任务都很重要。在此之前，这种性质已经出现在分离逻辑文献中的许多地方，但没有被系统地研究过。在本文中，我们开发了一个基于堆自动机的算法框架，使我们能够以统一的方式获得广泛的鲁棒性的渐近最优决策过程。我们实现了我们的框架的原型，并获得了令人鼓舞的结果，所有上述的鲁棒性。此外，我们证明了堆自动机的鲁棒性以外的适用性。我们将我们的算法框架应用于符号堆分离逻辑的模型检查和蕴涵问题。
We introduceheap automata, a formalism for automatic reasoning aboutrobustness propertiesof the symbolic heap fragment of separation logic with user-defined inductive predicates. Robustness properties, such as satisfiability, reachability, and acyclicity, are important for a wide range of reasoning tasks in automated program analysis and verification based on separation logic. Previously, such properties have appeared in many places in the separation logic literature, but have not been studied in a systematic manner. In this paper, we develop an algorithmic framework based on heap automata that allows us to derive asymptotically optimal decision procedures for a wide range of robustness properties in a uniform way.We implemented a prototype of our framework and obtained promising results for all of the aforementioned robustness properties.Further, we demonstrate the applicability of heap automata beyond robustness properties. We apply our algorithmic framework to themodel checkingand theentailment problemfor symbolic-heap separation logic.
登录
查看更多内容
DOI：
10.1145/2837614.2837621
发表时间：
2016-01
期刊：
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
J. Brotherston;Nikos Gorogiannis;M. Kanovich;R. Rowe
通讯作者：
J. Brotherston;Nikos Gorogiannis;M. Kanovich;R. Rowe
从分离逻辑到超边缘替换再返回
DOI：
--
发表时间：
2008
期刊：
International Conference on Graph Transformation
影响因子：
--
作者：
Mike Dodds
通讯作者：
Mike Dodds
通用循环定理证明者
影响因子：
0.6
作者：
J. Brotherston;Nikos Gorogiannis;R. Petersen
通讯作者：
R. Petersen
DOI：
10.1016/j.scico.2010.07.004
发表时间：
2012-08
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
W. Chin;C. David;Huu Hai Nguyen;S. Qin
通讯作者：
W. Chin;C. David;Huu Hai Nguyen;S. Qin
用于验证堆操作的森林自动机
影响因子：
0.8
作者：
P. Habermehl;L. Holík;Adam Rogalewicz;Jirí Simácek;Tomáš Vojnar
通讯作者：
Tomáš Vojnar