Lazy Abstraction for Higher-Order Program Verification
Taku Terao · 2018
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.