Automatic Termination Verification for Higher-Order Functional Programs
Automatic Termination Verification for Higher-Order Functional Programs
复制标题
DOI：
10.1007/978-3-642-54833-8_21
复制
发表时间：
2014-04
期刊：
影响因子：
--
通讯作者：
Takuya Kuwahara;Tachio Terauchi;Hiroshi Unno;N. Kobayashi
中科院分区：
文献类型：
--
作者：
Takuya Kuwahara;Tachio Terauchi;Hiroshi Unno;N. Kobayashi
我们提出了一个自动化的方法来验证终止高阶函数程序。我们的方法采用了最近通过转换不变量（又名二进制可达性分析）进行终止验证的想法，并且是完全自动化的。我们的方法能够很好地处理高阶程序的微妙方面，包括部分应用程序，间接调用，以及在函数闭包值上对函数进行排名。与以前的方法来自动终止验证功能程序，我们的方法是健全的和完整的，相对于底层的可达性分析和排名功能推理的健全性和完整性。我们已经实现了我们的方法的一个子集的OCaml语言的原型，我们已经证实，它能够自动验证终止一些非平凡的高阶程序。
We present an automated approach to verifying termination of higher-order functional programs. Our approach adopts the idea from the recent work on termination verification via transition invariants (a.k.a. binary reachability analysis), and is fully automated. Our approach is able to soundly handle the subtle aspects of higher-order programs, including partial applications, indirect calls, and ranking functions over function closure values. In contrast to the previous approaches to automated termination verification for functional programs, our approach is sound and complete, relative to the soundness and completeness of the underlying reachability analysis and ranking function inference. We have implemented a prototype of our approach for a subset of the OCaml language, and we have confirmed that it is able to automatically verify termination of some non-trivial higher-order programs.