Higher-order multi-parameter tree transducers and recursion schemes for program verification. (English) Zbl 1312.68136
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’10, Madrid, Spain, January 17–23, 2010. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-479-9). 495-508 (2010).
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q45 | Formal languages and automata |
Keywords:
higher-order recursion scheme; higher-order tree transducers; program verification; tree-processing programsReferences:
| [1] | K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3), 2007. · Zbl 1125.68068 |
| [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. 10.1007/11417170_5 · Zbl 1114.03006 |
| [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. · Zbl 1067.68541 |
| [4] | W. Dam. The io- and oi-hierarchies. Theoretical Computer Science, 20:95-207, 1982. · Zbl 0478.68012 |
| [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. · Zbl 1060.68062 |
| [7] | J. Engelfriet and H. Vogler. Macro tree transducers. J. Comput. Syst. Sci., 31(1):71-146, 1985. · Zbl 0588.68039 |
| [8] | J. Engelfriet and H. Vogler. High level tree transducers and iterated pushdown tree transducers. Acta Inf., 26(1/2):131-192, 1988. 10.1007/BF02915449 · Zbl 0633.68073 |
| [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.1145/113445.113468 |
| [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. 10.1109/LICS.2008.34 |
| [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. 10.1145/1101908.1101935 |
| [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. 10.1145/258948.258964 · Zbl 1369.68142 |
| [14] | A. Igarashi and N. Kobayashi. Resource usage analysis. ACM Transactions on Programming Languages and Systems, 27(2):264-313, 2005. 10.1145/1057387.1057390 |
| [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. 10.1145/1134744.1134751 |
| [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. · Zbl 0981.03012 |
| [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. · Zbl 1077.03508 |
| [18] | N. Kobayashi. Model-checking higher-order functions. In Proceedings of PPDP 2009. ACM Press, 2009. 10.1145/1599410.1599415 |
| [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. 10.1145/1480881.1480933 · Zbl 1315.68099 |
| [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. 10.1007/978-3-642-02930-1_19 · Zbl 1248.68334 |
| [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. 10.1109/LICS.2009.29 |
| [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. 10.1109/APSEC.2007.80 |
| [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. 10.1145/1065167.1065203 |
| [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. 10.1007/11965893_18 |
| [28] | T. Milo, D. Suciu, and V. Vianu. Typechecking for XML transformers. J. Comput. Syst. Sci., 66(1):66-97, 2003. 10.1016/S0022-0000(02)00030-2 · Zbl 1026.68045 |
| [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. 10.1145/1060745.1060809 |
| [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. 10.1007/978-3-540-31987-0_26 · Zbl 1108.68406 |
| [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. 10.1109/LICS.2006.38 |
| [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. 10.1007/s10515-009-0049-9 |
| [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. 10.1007/11737414_7 · Zbl 1185.68203 |
| [35] | R. Turner. An infinite hierarchy of term languages - an approach to mathematical complexity. In Proceedings of ICALP, pages 593-608, 1972. · Zbl 0278.68069 |
| [36] | P. Wadler. Deforestation: Transforming programs to eliminate trees. Theoretical Computer Science, 73(2):231-248, 1990. 10.1016/0304-3975(90)90147-A · Zbl 0701.68013 |
| [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. · Zbl 0305.68056 |
| [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. 10.1145/1368088.1368112 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
