Predicate abstraction and CEGAR for higher-order model checking
Predicate abstraction and CEGAR for higher-order model checking
复制标题
DOI：
10.1145/1993498.1993525
复制
发表时间：
2011-06
期刊：
影响因子：
--
通讯作者：
N. Kobayashi;Ryosuke Sato;Hiroshi Unno
中科院分区：
文献类型：
--
作者：
N. Kobayashi;Ryosuke Sato;Hiroshi Unno
高阶模型检测(更准确地说，是高阶递归方案的模型检测)近年来得到了广泛的研究，它可以自动判定用具有递归和有限数据域的简单类型λ演算编写的程序的性质。本文将谓词抽象和反例引导的抽象求精(CEGAR)形式化，用于高阶模型检测，使得对使用整数等无限数据域的程序进行自动验证成为可能。实现了一个基于该形式化的高阶函数式程序原型验证器，并对多个程序进行了测试。
Higher-order model checking (more precisely, the model checking of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties of programs written in the simply-typed λ-calculus with recursion and finite data domains. This paper formalizes predicate abstraction and counterexample-guided abstraction refinement (CEGAR) for higher-order model checking, enabling automatic verification of programs that use infinite data domains such as integers. A prototype verifier for higher-order functional programs based on the formalization has been implemented and tested for several programs.