Equivalence of Finite-Valued Symbolic Finite Transducers

  • Margus Veanes
  • Nikolaj Bjørner
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9609)


Symbolic Finite Transducers, or SFTs, is a representation of finite transducers that annotates transitions with logical formulas to denote sets of concrete transitions. This representation has practical advantages in applications for web security analysis, where it provides ways to succinctly represent web sanitizers that operate on large alphabets. More importantly, the representation is also conducive for efficient analysis using state-of-the-art theorem proving techniques. Equivalence checking plays a central role in deciding properties of SFTs such as idempotence and commutativity. We show that equivalence of finite-valued SFTs is decidable, i.e., when the number of possible outputs for a given input is bounded by a constant.


  1. 1.
    Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with Bek. In: USENIX Security, pp. 1–16 (2011)Google Scholar
  2. 2.
    Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjorner, N.: Symbolic finite state transducers: Algorithms and applications. In: POPL 2012. ACM, pp. 137–150 (2012)Google Scholar
  3. 3.
    Balzarotti, D., Cova, M., Felmetsger, V., Jovanovic, N., Kirda, E., Kruegel, C., Vigna, G.: Saner: Composing static and dynamic analysis to validate sanitization in web applications. In: SP (2008)Google Scholar
  4. 4.
    Yu, S.: Regular languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 1, pp. 41–110. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  5. 5.
    Demers, A., Keleman, C., Reusch, B.: On some decidable properties of finite state translations. Acta Informatica 17, 349–364 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Harrison, M.A.: Introduction to Formal Language Theory. Addison-Wesley, Reading (1978)zbMATHGoogle Scholar
  7. 7.
    Bjørner, N., Veanes, M.: Symbolic transducers. Microsoft Research, Technical Report MSR-TR-2011-3 (2011)Google Scholar
  8. 8.
    Ibarra, O.: The unsolvability of the equivalence problem for Efree NGSM’s with unary input (output) alphabet and applications. SIAM J. Comput. 4, 524–532 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Schützenberger, M.P.: Sur les relations rationnelles. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol. 33, pp. 209–213. Springer, Heidelberg (1975)Google Scholar
  10. 10.
    Culic, K., Karhumäki, J.: The equivalence problem for single-valued two-way transducers (on NPDT0L languages) is decidable. SIAM J. Comput. 16(2), 221–230 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Weber, A.: Decomposing finite-valued transducers and deciding their equivalence. SIAM J. Comput. 22(1), 175–202 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    D’Antoni, L., Veanes, M.: Equivalence of extended symbolic finite transducers. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 624–639. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  13. 13.
    Minamide, Y.: Static approximation of dynamically generated web pages. In: Proceedings of the 14th International Conference on the World Wide Web, WWW 2005, pp. 432–441 (2005)Google Scholar
  14. 14.
    Wassermann, G., Su, Z.: Sound and precise analysis of web applications for injection vulnerabilities. In: PLDI, pp. 32–41. ACM (2007)Google Scholar
  15. 15.
    Wassermann, G., Yu, D., Chander, A., Dhurjati, D., Inamura, H., Su, Z.: Dynamic test input generation for web applications. In: ISSTA (2008)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Microsoft ResearchRedmondUSA

Personalised recommendations