Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions
Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions
复制标题
具有归纳定义的符号堆循环证明的完整性
DOI：
10.1007/978-3-030-34175-6_19
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Kimura Daisuke
中科院分区：
文献类型：
--
作者：
Tatsuta Makoto;Nakazawa Koji;Kimura Daisuke
分离逻辑在理论和实践上都是成功的软件验证方法。符号堆的判定过程是其中的关键问题之一。本文提出了一个符号堆的循环证明系统，并证明了它的可靠性和完备性。锥归纳定义是从有界树宽归纳定义中通过对存在式施加一些限制而得到的，但它们仍然包括广泛的一类递归数据结构。利用证明搜索算法证明了其完备性，并给出了锥归纳定义下符号堆蕴涵的判定过程。该算法的时间复杂度为非确定性双指数。一个原型系统的算法已经实现，并给出了实验结果。
Separation logic is successful for software verification in both theory and practice. Decision procedure for symbolic heaps is one of the key issues. This paper proposes a cyclic proof system for symbolic heaps with general form of inductive definitions called cone inductive definitions, and shows its soundness and completeness. Cone inductive definitions are obtained from bounded-treewidth inductive definitions by imposing some restrictions for existentials, but they still include a wide class of recursive data structures. The completeness is proved by using a proof search algorithm and it also gives us a decision procedure for entailments of symbolic heaps with cone inductive definitions. The time complexity of the algorithm is nondeterministic double exponential. A prototype system for the algorithm has been implemented and experimental results are also presented.
登录
查看更多内容
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
16 值推理的免割系统
DOI：
--
发表时间：
2005
期刊：
Bulletin of the Section of Logic 34(4)
影响因子：
--
作者：
上出哲広;上出哲広;上出哲広;上出哲広;上出哲広;上出哲広;上出哲広
通讯作者：
上出哲広
通用循环定理证明者
影响因子：
0.6
作者：
J. Brotherston;Nikos Gorogiannis;R. Petersen
通讯作者：
R. Petersen
循环算术相当于皮亚诺算术
DOI：
10.1007/978-3-662-54458-7_17
发表时间：
2017
期刊：
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
影响因子：
--
作者：
A. Simpson
通讯作者：
A. Simpson
DOI：
10.1109/lics.2017.8005114
发表时间：
2017
期刊：
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
影响因子：
--
作者：
S. Berardi;M. Tatsuta
通讯作者：
M. Tatsuta