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 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. © 2010 Springer-Verlag.
CITATION STYLE
Unno, H., Tabuchi, N., & Kobayashi, N. (2010). Verification of tree-processing programs via higher-order model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6461 LNCS, pp. 312–327). https://doi.org/10.1007/978-3-642-17164-2_22
Mendeley helps you to discover research relevant for your work.