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 worstcase complexity, practical algorithms have been developed that work well for typical inputs that arise in program verification. Even the stateof-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.