Verification of Tree-Processing Programs via Higher-Order Model Checking

Abstract. We propose a new method to verify that a higher-order, treeprocessing 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 transformed 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 programmer. We have proved the soundness of the method and implemented a prototype verifier.

• Type: Conference
• Year: 2010
• Where: APLAS
• Authors: Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
• Keywords: APLAS 2010, Data Structures, Functional Programs, Programming Languages, Verification Problems