No CrossRef data available.
Article contents
Verification of tree-processing programs via higher-order mode checking†
Published online by Cambridge University Press: 10 November 2014
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 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
- Paper
- Information
- Mathematical Structures in Computer Science , Volume 25 , Issue 4: APLAS 2010 , May 2015 , pp. 841 - 866
- Copyright
- Copyright © Cambridge University Press 2014
Footnotes
Revised and extended version of (Unno et al. 2010).