Higher-order multi-parameter tree transducers and recursion schemes for program verification

ABSTRACT

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, and then uses (an extension of)Kobayashi's algorithm for model-checking recursion schemes. While the algorithm is incomplete (indeed, as we show in the paper, the verification problem is undecidable in general), it is sound and complete for a subclass of HMTTs called linear HMTTs . We have applied our HMTT verification algorithm to various program verification problems and obtained promising results.

References

1. K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3), 2007.
2. K. Aehlig, J. G. de Miranda, and C.-H. L. Ong. The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable. In TLCA 2005, volume 3461 of Lecture Notes in Computer Science, pages 39--54. Springer-Verlag, 2005.
3. A. S. Christensen, A. Møller, and M. I. Schwartzbach. Precise analysis of string expressions. In Static Analysis, 10th International Symposium, SAS 2003, volume 2694 of Lecture Notes in Computer Science, pages 1--18. Springer-Verlag, 2003.
4. W. Dam. The io- and oi-hierarchies. Theoretical Computer Science, 20:95--207, 1982.
5. R. Davies. Practical refinement-type checking. PhD thesis, Pittsburgh, PA, USA, 2005.
6. J. Engelfriet and S. Maneth. A comparison of pebble tree transducers with macro tree transducers. Acta Inf., 39(9):613--698, 2003.
7. J. Engelfriet and H. Vogler. Macro tree transducers. J. Comput. Syst. Sci., 31(1):71--146, 1985.
8. J. Engelfriet and H. Vogler. High level tree transducers and iterated pushdown tree transducers. Acta Inf., 26(1/2):131--192, 1988.
9. T. Freeman and F. Pfenning. Refinement types forML. In Proceedings of ACMSIGPLAN Conference on Programming Language Design and Implementation, pages 268--277. ACM Press, 1991.
10. A. Frisch and H. Hosoya. Towards practical typechecking for macro tree transducers. In Database Programming Languages, 11th International Symposium (DBPL 2007), volume 4797 of Lecture Notes in Computer Science, pages 246--260. Springer-Verlag, 2007.
11. M. Hague, A. Murawski, C.-H. L. Ong, and O. Serre. Collapsible pushdown automata and recursion schemes. In Proceedings of 23rd Annual IEEE Symposium on Logic in Computer Science, pages 452--461. IEEE Computer Society, 2008.
12. W. G. J. Halfond and A. Orso. Amnesia: analysis and monitoring for neutralizing sql-injection attacks. In ASE '05: Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, pages 174--183, New York, NY, USA, 2005. ACM.
13. Z. Hu, H. Iwasaki, M. Takeichi, and A. Takano. Tupling calculation eliminates multiple data traversals. In Proceedings of International Conference on Functional Programming, pages 164--175, 1997.
14. A. Igarashi and N. Kobayashi. Resource usage analysis. ACM Transactions on Programming Languages and Systems, 27(2):264--313, 2005.
15. N. Jovanovic, C. Kruegel, and E. Kirda. Precise alias analysis for static detection of web application vulnerabilities. In PLAS '06: Proceedings of the 2006 workshop on Programming languages and analysis for security, pages 27--36, New York, NY, USA, 2006. ACM.
16. T. Knapik, D. Niwinski, and P. Urzyczyn. Deciding monadic theories of hyperalgebraic trees. In TLCA 2001, volume 2044 of Lecture Notes in Computer Science, pages 253--267. Springer-Verlag, 2001.
17. T. Knapik, D. Niwinski, and P. Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS 2002, volume 2303 of Lecture Notes in Computer Science, pages 205--222. Springer-Verlag, 2002.
18. N. Kobayashi. Model-checking higher-order functions. In Proceedings of PPDP 2009. ACM Press, 2009.
19. N. Kobayashi. TRECS. http://www.kb.ecei.tohoku.ac.jp/~koba/trecs/, 2009.
20. N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pages 416--428, 2009.
21. N. Kobayashi and C.-H. L. Ong. Complexity of model checking recursion schemes for fragments of the modal mu-calculus. In Proceedings of ICALP 2009, volume 5556 of Lecture Notes in Computer Science. Springer-Verlag, 2009.
22. N. Kobayashi and C.-H. L. Ong. A type system equivalent to themodal mu-calculus model checking of higher-order recursion schemes. In Proceedings of LICS 2009, pages 179--188. IEEE Computer Society Press, 2009.
23. N. Kobayashi, N. Tabuchi, and H. Unno. Higher-order multiparameter tree transducers and recursion schemes for program verification. A longer version, available from http://www.kb.ecei.tohoku.ac.jp/~koba/papers/hmtt.pdf, 2009.
24. M. Koganeyama, N. Tabuchi, and T. Tateishi. Reducing unnecessary conservativeness in access rights analysis with string analysis. In APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference, pages 438--445, Washington, DC, USA, 2007. IEEE Computer Society.
25. S. Maneth, A. Berlea, T. Perst, and H. Seidl. XML type checking with macro tree transducers. In Proceedings of the Twenty-fourth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS 2005), pages 283--294, 2005.
26. S. Maneth and K. Nakano. XML type checking for macro tree transducers with holes. In Programming Language Technologies for XML (PLAN-X), 2008.
27. S. Maneth, T. Perst, and H. Seidl. Exact XML type checking in polynomial time. In ICDT 2007, volume 4353 of Lecture Notes in Computer Science, pages 254--268. Springer-Verlag, 2007.
28. T. Milo, D. Suciu, and V. Vianu. Typechecking for XML transformers. J. Comput. Syst. Sci., 66(1):66--97, 2003.
29. Y. Minamide. Static approximation of dynamically generated web pages. In Proceedings of the 14th international conference on World Wide Web (WWW 2005), pages 432--441. ACM Press, 2005.
30. M. Naik. A type system equivalent to a model checker. Master Thesis, Purdue University.
31. M. Naik and J. Palsberg. A type system equivalent to a model checker. In ESOP 2005, volume 3444 of Lecture Notes in Computer Science, pages 374--388. Springer-Verlag, 2005.
32. C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In LICS 2006, pages 81--90. IEEE Computer Society Press, 2006.
33. J. Sawin and A. Rountev. Improving static resolution of dynamic class loading in java using dynamically gathered environment information. Automated Software Engg., 16(2):357--381, 2009.
34. A. Tozawa. XML type checking using high-level tree transducer. In Functional and Logic Programming, 8th International Symposium (FLOPS 2006), volume 3945 of Lecture Notes in Computer Science, pages 81--96. Springer-Verlag, 2006.
35. R. Turner. An infinite hierarchy of term languages - an approach to mathematical complexity. In Proceedings of ICALP, pages 593--608, 1972.
36. P. Wadler. Deforestation: Transforming programs to eliminate trees. Theoretical Computer Science, 73(2):231--248, 1990.
37. M. Wand. An algebraic formulation of the chomsky hierarchy. In Category Theory Applied to Computation and Control, volume 25 of Lecture Notes in Computer Science, pages 209--213. Springer-Verlag, 1974.
38. G. Wassermann and Z. Su. Static detection of cross-site scripting vulnerabilities. In ICSE '08: Proceedings of the 30th international conference on Software engineering, pages 171--180, New York, NY, USA, 2008. ACM.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning

      • Program verification