Verification of Tree-Processing Programs via Higher-Order Model Checking Hiroshi Unno, Naoshi Tabuchi

Abstract. We propose a new method to verify that a higher-order, tree-processing functional program conforms to an input/output specification. Our method reduces the verification problem to multiple verification problems for higher-order multi-tree transducers, which are then trans-formed into higher-order recursion schemes and model-checked. Unlike previous methods, our new method can deal with arbitrary higher-order functional programs manipulating algebraic data structures, as long as certain invariants on intermediate data structures are provided by a pro-grammer. We have proved the soundness of the method and implemented a prototype verifier.