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, ...

• Type: Conference
• Year: 2010
• Where: POPL
• Authors: Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
• Keywords: HMTT Verification Algorithm, Incomplete Verification Algorithm, POPL 2010, Programming Languages, Verification Problem