A ZDD-based Efficient Higher-order Model Checking Algorithm

Abstract. The model checking of higher-order recursion schemes, aka. higher-order model checking, has recently been applied to automated verification of higher-order programs. Despite its extremely high worst-case complexity, practical algorithms have been developed that work well for typical inputs that arise in program verification. Even the state-of-the-art algorithms are, however, not scalable enough for verification of thousands or millions of lines of programs. We, therefore, propose a new higher-order model checking algorithm. It is based on Broadbent and Kobayashi’s type and saturation-based algorithm HorSat, but we make two significant modifications. First, unlike HorSat, we collect flow information (which is necessary for optimization) in linear time by using a sub-transitive flow graph. Thanks to this, the resulting algorithm runs in almost linear time under a fixed-parameter assumption. Secondly, we employ zero-suppressed binary decision diagrams to efficiently represent and propagate type information. We have confirmed through experiments that the new algorithm is more scalable for several families of inputs than the state-of-the-art higher-order model checkers HorSat and Preface.