Model-Checking Higher-Order Functions

We propose a novel type-based model checking algorithm for higher-order recursion schemes. As shown by Kobayashi, verification problems of higher-order functional programs can easily be translated into model checking problems of recursion schemes. Thus, the model checking algorithm serves as a basis for verification of higher-order functional programs. To our knowledge, this is the first practical algorithm for model checking recursion schemes: all the previous algorithms always suffer from the n-EXPTIME bottleneck, not only in the worst case, and there was no implementation of the algorithms. We have implemented a model checker for recursion schemes based on the proposed algorithm, and applied it to verification of functional programs, including reachability, flow analysis and resource usage verification problems. According to our experiments, the model checker is surprisingly fast: it could automatically verify a number of small but tricky higher-order functional programs in less than a second.