Temporal Verification of Higher-Order Functional Programs
Temporal Verification of Higher-Order Functional Programs
复制标题
高阶函数程序的时间验证
DOI：
10.1145/2837614.2837667
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
and Hiroshi Unno
中科院分区：
文献类型：
--
作者：
Akihiro Murase;Tachio Terauchi;Naoki Kobayashi;Ryosuke Sato;and Hiroshi Unno
我们提出了一种自动验证高阶函数程序任意omega-正则性质的方法。以前针对这类程序提出的自动化方法只能处理安全属性或终止，而我们的方法是第一个能够验证任意omega-Regular活性属性的方法。我们的方法是自动机理论，并将我们最近发表在ESOP 2014上的基于二进制可达性的方法用于高阶函数程序的自动终止验证的工作扩展到公平终止。在这项工作中，我们证明了检验“调用关系”的析取良基(传递闭包)是健全的和完全的终止性。然而，公平终止的扩展是棘手的，因为检查公平调用关系的析取良好基础的直接扩展被证明是不可靠的，正如我们将在论文中说明的那样。粗略地说，我们的解决方案是检查转换关系而不是调用关系上的公平性，并传播信息来确定何时检查调用关系上的析取良基是必要和充分的。我们证明了我们的方法是健全和完整的。我们已经实现了我们的方法的一个原型，并确认它能够自动验证一些非平凡的高阶程序的活性性质。
We present an automated approach to verifying arbitrary omega-regular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the ``calling relation'' is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.