Verifying Higher-Order Functional Programs with Tree Automata

This paper describes a fully automatic technique for verifying properties of higher-order functional programs. Functional programs are modelled with term rewriting systems and tree automata are used to model reachable program states. From a tree automaton representing the initial state, it is possible to define a completion algorithm on tree automata for approximating the output set of the program to verify. We define a subclass of higher-order functional programs for which the completion is guaranteed to terminate. Furthermore, since precision of the completion is fixed by a set of equations, we also propose an algorithm to automatically generate sets of equations by iterative refinement. We present some experiments showing that the resulting verification technique is complementary and extends several state-of-the-art model-checking approaches for higher-order functional programs.