Towards a scalable software model checker for higher-order programs

Abstract

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.