Sciweavers

Share
APLAS
2010
ACM

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

10 years 1 months ago
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.
Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
Added 05 Dec 2010
Updated 05 Dec 2010
Type Conference
Year 2010
Where APLAS
Authors Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
Comments (0)
books