Higher-Order Model Checking in Direct Style
Higher-Order Model Checking in Direct Style
复制标题
直接风格的高阶模型检查
DOI：
10.1007/978-3-319-47958-3_16
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
and Naoki Kobayashi
中科院分区：
文献类型：
--
作者：
Taku Terao;Taskeshi Tsukada;and Naoki Kobayashi
高阶模型检测，或高阶递归模式的模型检测，最近已被应用于功能程序的全自动验证。以前的方法是间接的，在这个意义上，高阶函数程序首先抽象为（按值调用）高阶布尔程序，然后进一步翻译为高阶递归方案（本质上是按名称调用程序）和模型检查。这些多步转换导致了许多问题，如代码爆炸。在本文中，我们提倡一种更直接的方法，高阶布尔程序直接模型检查，而不转换为高阶递归计划。为此，我们提出了一个高阶按值调用布尔程序的模型检测算法，并证明了算法的正确性。实验结果表明，在大规模的实例中，我们的原型实现优于间接方法。
Higher-order model checking, or model checking of higher-order recursion schemes, has been recently applied to fully automated verification of functional programs. The previous approach has beenindirect, in the sense that higher-order functional programs are first abstracted to (call-by-value) higher-order Boolean programs, and then further translated to higher-order recursion schemes (which are essentially call-by-nameprograms) and model checked. These multi-step transformations caused a number of problems such as code explosion. In this paper, we advocate a moredirectapproach, where higher-order Boolean programs are directly model checked, without transformation to higher-order recursion schemes. To this end, we develop a model checking algorithm for higher-order call-by-value Boolean programs, and prove its correctness. According to experiments, our prototype implementation outperforms the indirect method for large instances.