Symbolic transducers are useful in the context of web security as they form the foundation for sanitization of potentially malicious data. We define Symbolic Tree Transducers as a generalization of Regular Transducers as finite state input-output tree automata with logical constraints over a parametric background theory. We examine key closure properties of Symbolic Tree Transducers and we develop a composition algorithm and an equivalence decision procedure for linear single-valued transducers.


Equivalence Check Functional Program Input Tree Tree Automaton Tree Transducer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Cerný, P.: Streaming transducers for algorithmic verification of single-pass list-processing programs. In: 38th ACM SIGACT-SIGPLAN Symposium on Princples of Programming Languages (POPL 2011), pp. 599–610. ACM (2011)Google Scholar
  2. 2.
    Arnold, A., Dauchet, M.: Bi-transductions de forêts. In: Proc. 3rd International Colloquium on Automata, Languages and Programming (ICALP 1976), pp. 74–86. Edinburgh University Press, Edinburgh (1976)Google Scholar
  3. 3.
    Baker, B.S.: Composition of top-down and bottom-up tree transductions. Inform. and Control 41, 186–213 (1979)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Choffrut, C.: Minimizing subsequential transducers: a survey. Theoretical Computer Science 292(1), 131–143 (2003)MathSciNetzbMATHCrossRefGoogle Scholar
  5. 5.
    Courcelle, B., Franchi-Zannettacchi, P.: Attribute grammars and recursive program schemes. Theoretical Computer Science 17, 163–191 (1982)MathSciNetCrossRefGoogle Scholar
  6. 6.
    de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Engelfriet, J.: Bottom-up and top-down tree transformations – a comparison. Math. Systems Theory 9, 198–231 (1975)MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    Engelfriet, J.: Some open questions and recent results on tree transducers and tree languages. In: Book, R.V. (ed.) Formal Language Theory, pp. 241–286. Academic Press, New York (1980)Google Scholar
  9. 9.
    Engelfriet, J., Maneth, S.: Macro tree transducers, attribute grammars, and mso definable tree translations. Information and Computation 154, 34–91 (1999)MathSciNetzbMATHCrossRefGoogle Scholar
  10. 10.
    Engelfriet, J., Maneth, S.: A comparison of pebble tree transducers with macro tree transducers. Acta Informatica 39 (2003)Google Scholar
  11. 11.
    Engelfriet, J., Maneth, S., Seidl, H.: Deciding equivalence of top-down XML transformations in polynomial time. Journal of Computer and System Science 75(5), 271–286 (2009)MathSciNetzbMATHCrossRefGoogle Scholar
  12. 12.
    Engelfriet, J., Vogler, H.: Macro tree transducers. J. Comp. and Syst. Sci. 31, 71–146 (1985)MathSciNetzbMATHCrossRefGoogle Scholar
  13. 13.
    Esik, Z.: Decidability results concerning tree transducers. Acta Cybernetica 5, 1–20 (1980)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Fülöp, Z.: On attributed tree transducers. Acta Cybernetica 5, 261–279 (1981)zbMATHGoogle Scholar
  15. 15.
    Fülöp, Z., Vogler, H.: Syntax-Directed Semantics: Formal Models Based on Tree Transducers. EATCS. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  16. 16.
    Gécseg, F., Steinby, M.: Tree Automata. Akadémiai Kiadó, Budapest (1984)zbMATHGoogle Scholar
  17. 17.
    Griffiths, T.: The unsolvability of the equivalence problem for Λ-free nondeterministic generalized machines. J. ACM 15, 409–413 (1968)zbMATHCrossRefGoogle Scholar
  18. 18.
    Hodges, W.: Model theory. Cambridge Univ. Press (1995)Google Scholar
  19. 19.
    Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with Bek. In: 20th USENIX Security Symposium, pp. 1–16. USENIX Association, San Francisco (2011)Google Scholar
  20. 20.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison Wesley (1979)Google Scholar
  21. 21.
    Ibarra, O.: The unsolvability of the equivalence problem for Efree NGSM’s with unary input (output) alphabet and applications. SIAM Journal on Computing 4, 524–532 (1978)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Inaba, K., Hosoya, H.: Multi-return macro tree transducers. In: Proc. 6th ACM SIGPLAN Workshop on Programming Language Technologies for XML, San Francisco, California (January 2008)Google Scholar
  23. 23.
    Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 495–508. ACM (2010)Google Scholar
  24. 24.
    Laurence, G., Lemay, A., Niehren, J., Staworko, S., Tommasi, M.: Normalization of Sequential Top-Down Tree-to-Word Transducers. In: Dediu, A.-H., Inenaga, S., Martín-Vide, C. (eds.) LATA 2011. LNCS, vol. 6638, pp. 354–365. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  25. 25.
    Maletti, A., Graehl, J., Hopkins, M., Knight, K.: The power of extended top-down tree transducers. SIAM J. Comput. 39, 410–430 (2009)MathSciNetzbMATHCrossRefGoogle Scholar
  26. 26.
    Milo, T., Suciu, D., Vianu, V.: Typechecking for XML transformers. In: Proc. 19th ACM Symposium on Principles of Database Systems (PODS 2000), pp. 11–22. ACM (2000)Google Scholar
  27. 27.
    Noord, G.V., Gerdemann, D.: Finite state transducers with predicates and identities. Grammars 4, 263–286 (2001)MathSciNetzbMATHCrossRefGoogle Scholar
  28. 28.
    Ong, C.-H.L., Ramsay, S.J.: Verifying higher-order functional programs with pattern-matching algebraic data types. In: 38th ACM SIGACT-SIGPLAN Symposium on Princples of Programming Languages (POPL 2011), pp. 587–598. ACM (2011)Google Scholar
  29. 29.
    Perst, T., Seidl, H.: Macro forest transducers. Information Processing Letters 89(3), 141–149 (2004)MathSciNetzbMATHCrossRefGoogle Scholar
  30. 30.
    Rounds, W.C.: Context-free grammars on trees. In: Proc. ACM Symp. on Theory of Comput., pp. 143–148. ACM (1969)Google Scholar
  31. 31.
    Seidl, H.: Equivalence of finite-valued tree transducers is decidable. Math. Systems Theory 27, 285–346 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  32. 32.
    Thatcher, J.W.: Generalized sequential machine maps. J. Comput. Syst. Sci. 4, 339–367 (1970)MathSciNetzbMATHCrossRefGoogle Scholar
  33. 33.
    Veanes, M., Bjørner, N.: Symbolic tree automata. Submitted to Information Processing Letters (2011)Google Scholar
  34. 34.
    Veanes, M., Bjørner, N., de Moura, L.: Symbolic Automata Constraint Solving. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 640–654. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  35. 35.
    Veanes, M., de Halleux, P., Tillmann, N.: Rex: Symbolic regular expression explorer. In: Third International Conference on Software Testing, Verification and Validation (ICST 2010), pp. 498–507. IEEE Computer Society (2010)Google Scholar
  36. 36.
    Yu, S.: Regular languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 1, pp. 41–110. Springer, Heidelberg (1997)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Margus Veanes
    • 1
  • Nikolaj Bjørner
    • 1
  1. 1.Microsoft ResearchRedmondUSA

Personalised recommendations