Hostname: page-component-586b7cd67f-t8hqh Total loading time: 0 Render date: 2024-11-24T23:14:12.843Z Has data issue: false hasContentIssue false

Verification of tree-processing programs via higher-order mode checking

Published online by Cambridge University Press:  10 November 2014

HIROSHI UNNO
Affiliation:
Department of Computer Science, Graduate School of Systems and Information Engineering, University of Tsukuba, 1-1-1 Tennodai, Tsukuba-shi, Ibaraki 305-8573, Japan Email: [email protected]
NAOSHI TABUCHI
Affiliation:
Trek Inc., 14-15 Futsuka-machi, Aoba-ku, Sendai-shi, Miyagi 980-0802, Japan Email: [email protected]
NAOKI KOBAYASHI
Affiliation:
Department of Computer Science, Graduate School of Information Science and Technology, The University of Tokyo, 7-3-1 Hongo, Bunkyo-ku, Tokyo 113-0033, Japan Email: [email protected]

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
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

Revised and extended version of (Unno et al. 2010).

References

Aehlig, K., de Miranda, J. G. and Luke Ong, C.-H.. (2005) The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable. In:TLCA'05, Springer Lecture Notes in Computer Science, 3461 3954.CrossRefGoogle Scholar
Benzaken, V., Castagna, G. and Frisch, A. (2003) CDuce: An XML-centric general-purpose language. In: ICFP '03, ACM 5163.CrossRefGoogle Scholar
Christensen, A. S., Møller, A. and Schwartzbach, M. I. (2003) Precise analysis of string expressions. In: SAS'03, Springer Lecture Notes in Computer Science 2694 118.CrossRefGoogle Scholar
Davies, R. (2005) Practical Refinement-Type Checking, Ph.D. thesis, Carnegie Mellon University, Chair-Pfenning, Frank.Google Scholar
Engelfriet, J. and Vogler, H. (1985) Macro tree transducers. Journal of Computer and System Sciences 31 (1)71146.CrossRefGoogle Scholar
Engelfriet, J. and Vogler, H. (1988) High level tree transducers and iterated pushdown tree transducers. Acta Informatica 26 (1/2)131192.CrossRefGoogle Scholar
Freeman, T. and Pfenning, F. (1991) Refinement types for ML. In: PLDI '91, ACM 268277.CrossRefGoogle Scholar
Hosoya, H. and Pierce, B. C. (2003) XDuce: A statically typed XML processing language. ACM Transactions on Internet Technology 3 (2)117148.CrossRefGoogle Scholar
Hosoya, H., Vouillon, J. and Pierce, B. C. (2000) Regular expression types for XML. In: ICFP '00, ACM 1122.CrossRefGoogle Scholar
Hosoya, H., Frisch, A. and Castagna, G. (2009) Parametric polymorphism for XML. ACM Transactions on Programming Languages and Systems 32 (1)156.CrossRefGoogle Scholar
Jones, N. D. and Andersen, N. (2007) Flow analysis of lazy higher-order functional programs. Theoretical Computer Science 375 (1–3)120136.CrossRefGoogle Scholar
Knapik, T., Niwinski, D. and Urzyczyn, P. (2002) Higher-order pushdown trees are easy. In: FoSSaCS'02, Springer Lecture Notes in Computer Science 2303 205222.CrossRefGoogle Scholar
Kobayashi, N. and Ong, C.-H. L. (2009) A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: LICS '09, IEEE 179188.Google Scholar
Kobayashi, N., Tabuchi, N. and Unno, H. (2010) Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: POPL '10, ACM 495508.CrossRefGoogle Scholar
Kobayashi, N. (2009a) Types and higher-order recursion schemes for verification of higher-order programs. In: POPL '09, ACM 416428.CrossRefGoogle Scholar
Kobayashi, N. (2009b) Model-checking higher-order functions. In: PPDP '09, ACM 2536.CrossRefGoogle Scholar
Kochems, J. and Ong, C.-H. L. (2011) Improved functional flow and reachability analyses using indexed linear tree grammars. In: RTA2011.Google Scholar
Maneth, S., Berlea, A., Perst, T. and Seidl, H. (2005) XML type checking with macro tree transducers. In: PODS '05, ACM 283294.CrossRefGoogle Scholar
Milo, T., Suciu, D. and Vianu, V. (2003) Typechecking for XML transformers. Journal of Computer and System Sciences 66 (1)6697.CrossRefGoogle Scholar
Minamide, Y. (2005) Static approximation of dynamically generated web pages. In: WWW '05, ACM 432441.CrossRefGoogle Scholar
Ong, C.-H. L. and Ramsay, S. J. (2011) Verifying higher-order functional programs with pattern-matching algebraic data types. In: POPL '11, ACM 587598.CrossRefGoogle Scholar
Ong, C.-H. L. (2006) On model-checking trees generated by higher-order recursion schemes. In: LICS '06, IEEE 8190.Google Scholar
Schmidt, A., Waas, F., Kersten, M., Carey, M. J., Manolescu, I. and Busse, R. (2002) XMark: A benchmark for XML data management. In: VLDB '02, VLDB Endowment 974985.Google Scholar
Tabuchi, N., Kobayashi, N. and Unno, H. (2011) Inference of tree data structure invariant based on language identification from samples. (Available at http://www.kb.is.s.u-tokyo.ac.jp/~uhiro/.)Google Scholar
Tozawa, A. (2006) XML type checking using high-level tree transducer. In: FLOPS'06, Springer Lecture Notes in Computer Science 3945 8196.CrossRefGoogle Scholar
Unno, H., Tabuchi, N. and Kobayashi, N. (2010) Verification of tree-processing programs via higher-order model checking. In: APLAS'10, Springer Lecture Notes in Computer Science 6461 312327.CrossRefGoogle Scholar