Sciweavers

POPL
2010
ACM

Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification

14 years 1 months ago
Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification
We introduce higher-order, multi-parameter, tree transducers (HMTTs, for short), which are kinds of higher-order tree transducers that take input trees and output a (possibly infinite) tree. We study the problem of checking whether the tree generated by a given HMTT conforms to a given output specification, provided that the input trees conform to input specifications (where both input/output specifications are regular tree languages). HMTTs subsume higher-order recursion schemes and ordinary tree transducers, so that their verification has a number of potential applications to verification of functional programs using recursive data structures, including resource usage verification, string analysis, and exact type-checking of XML-processing programs. We propose a sound but incomplete verification algorithm for the HMTT verification problem: the algorithm reduces the verification problem to a model-checking problem for higher-order recursion schemes extended with finite data domains, ...
Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
Added 01 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where POPL
Authors Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
Comments (0)