Automata-based abstraction for automated verification of higher-order tree-processing programs

Abstract

Higher-order model checking has been recently applied to automated verification of higher-order functional programs, but there have been difficulties in dealing with algebraic data types such as lists and trees. To remedy the problem, we propose an automata-based abstraction of tree data, and a counterexample-guided refinement of the abstraction. By combining them with higher-order model checking, we can construct a fully-automated verification tool for higher-order, tree-processing functional programs. We formalize the verification method, prove its correctness, and report experimental results.