Lazy Abstraction for Higher-Order Program Verification
Lazy Abstraction for Higher-Order Program Verification
复制标题
高阶程序验证的惰性抽象
DOI：
10.1145/3236950.3236969
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Terao Taku
中科院分区：
文献类型：
--
作者：
Shinsuke Satoi;Yoh Iwasa;Shinsuke Satoi;Shinsuke Satoi;Terao Taku
提出了一种用于函数式程序验证的惰性抽象算法。惰性抽象方法的特点是将谓词抽象和模型检测融合在一起，对不可达配置的抽象进行剪枝。我们定义了一个抽象的语义，其特征在于懒惰的抽象算法的精度，并证明了我们的验证方法的可靠性和我们的抽象细化算法的进度属性。我们已经实现了我们的方法的原型，并通过实验证实，验证的总效率提高，与以前的渴望抽象方法相比。
This paper proposes a lazy abstraction algorithm for verification of functional programs. The feature of the lazy abstraction method is that the predicate abstraction and the model checking are fused, and that abstractions for unreachable configurations are pruned. We define an abstract semantics that characterizes the precision of the lazy abstraction algorithm, and prove the soundness of our verification method and the progress property of our abstraction refinement algorithm. We have implemented a prototype of our method, and confirmed through experiments that the total efficiency of verification is improved, compared with previous eager abstraction methods.