Towards a scalable software model checker for higher-order programs

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 combin- ing higher-order model checking, predicate abstraction, and CE- GAR. This can be viewed as a higher-order counterpart of previ- ous software model checkers for imperative languages like BLAST and SLAM. The naïve application of the proposed approach, how- ever, 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.