Towards a scalable software model checker for higher-order programs
Towards a scalable software model checker for higher-order programs
复制标题
面向高阶程序的可扩展软件模型检查器
DOI：
10.1145/2426890.2426900
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Naoki Kobayashi
中科院分区：
文献类型：
--
作者：
Ryosuke Sato;Hiroshi Unno;Naoki Kobayashi
在我们最近的论文中，我们展示了如何通过结合高阶模型检查，谓词抽象和CEGAR，为函数语言ML的一个小子集构建一个全自动程序验证工具（所谓的“软件模型检查器”）。这可以被看作是以前的软件模型检查器的高阶对应物，用于命令式语言，如BLAST和SLAM。然而，所提出的方法的天真的应用程序，遭受可扩展性的问题，无论是在效率和支持的语言功能。为了获得更可扩展的软件模型检查器的全面功能语言，我们提出了一系列的优化和扩展以前的方法。其中，我们介绍了（i）选择性CPS转换，（ii）选择性谓词抽象，（iii）细化谓词发现作为优化技术;并提出（iv）递归数据结构和控制操作的函数编码，以支持更大的ML子集。我们已经实现了所提出的方法，并取得了可喜的成果。
In our recent paper, we have shown how to construct a fully-automated program verification tool (so called a "software model checker") for a tiny subset of functional language ML, by combining higher-order model checking, predicate abstraction, and CEGAR. This can be viewed as a higher-order counterpart of previous software model checkers for imperative languages like BLAST and SLAM. The naive application of the proposed approach, however, suffered from scalability problems, both in terms of efficiency and supported language features. To obtain more scalable software model checkers for full-scale functional languages, we propose a series of optimizations and extensions of the previous approach. Among others, we introduce (i) selective CPS transformation,(ii) selective predicate abstraction, and (iii) refined predicate discovery as optimization techniques; and propose (iv) functional encoding of recursive data structures and control operations to support a larger subset of ML. We have implemented the proposed methods, and obtained promising results.