Higher-Order Model Checking: An Overview

Abstract—Higher-order model checking is about the model checking of trees generated by recursion schemes. The past fifteen years or so have seen considerable progress in both theory and practice. Advances have been made in determining the expressive power of recursion schemes and other higher-order families of generators, automata-theoretic characterisations of these generator families, and the algorithmics and semantics of higher-order model checking and allied methods of formal analysis. Because the trees generated by recursion schemes are computation trees of higher-order functional programs, higher-order model checking provides a foundation for model checkers of such programming languages as Haskell, F # and Erlang. This paper aims to give an overview of recent developments in higher-order model checking. I