Model checking liveness properties of higher-order functional programs

Abstract

Recent advances in the model checking of recursion schemes have opened the prospect of a model checking approach to the verification of higher-order functional programs. We formulate the Resource Usage Verification Problem in a general (liveness) setting, where good behaviours are specified by alternating parity (word) automata; and we give a sound and complete decision procedure by reduction to the problem of model checking higher-order recursion schemes (HORS) against alternating parity tree automata. Extending Kobayashi's type-inference approach, we present an efficient algorithm for deciding a restriction of the model checking problem in which properties are expressed by alternating weak tree automata (and hence all CTL formulas). We have constructed a model checker, THORS, that implements our algorithm and a number of optimisations. Despite the hugely challenging worst-case time complexity, THORS performs remarkably well on small examples, even up to order 5. To our knowledge, this is the first model checker for HORS which allows for the specification of tree automata with a non-trivial acceptance condition, including all CTL properties.