Completeness of Cyclic Proofs for Symbolic Heaps
Completeness of Cyclic Proofs for Symbolic Heaps
复制标题
符号堆循环证明的完整性
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
D. Kimura
中科院分区：
文献类型：
--
作者：
M. Tatsuta;Koji Nakazawa;D. Kimura
分离逻辑对于软件验证在理论和实践上都是成功的。符号堆的决策过程是关键问题之一。本文提出了一种具有归纳定义一般形式的符号堆循环证明系统，并证明了其健全性和完整性。还给出了具有归纳定义的符号堆蕴涵的决策过程。带有归纳定义的符号堆蕴涵的可判定性是一个重要的问题。循环证明系统的完整性也是一个重要问题。本文的结果回答了这两个问题。该决策过程是可行的，因为它是不确定的双指数时间复杂度。
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, and shows its soundness and completeness. The decision procedure for entailments of symbolic heaps with inductive definitions is also given. Decidability for entailments of symbolic heaps with inductive definitions is an important question. Completeness of cyclic proof systems is also an important question. The results of this paper answer both questions. The decision procedure is feasible since it is nondeterministic double-exponential time complexity.
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：
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