Loris D'Antoni
Margus Veanes
Benjamin Livshits
ABSTRACT
Tree automata and tree transducers are used in a wide range of applications in software engineering, from XML processing to language type-checking. While these formalisms are of immense practical use, they can only model finite alphabets, and since many real-world applications operate over infinite domains such as integers, this is often a limitation. To overcome this problem we augment tree automata and transducers with symbolic alphabets represented as parametric theories. Admitting infinite alphabets makes these models more general and succinct than their classical counterparts. Despite this, we show how the main operations, such as composition and language equivalence, remain computable given a decision procedure for the alphabet theory.
We introduce a high-level language called Fast that acts as a front-end for the above formalisms. Fast supports symbolic alphabets through tight integration with state-of-the-art satisfiability modulo theory (SMT) solvers. We demonstrate our techniques on practical case studies, covering a wide range of applications.
- R. Alur and L. D'Antoni. Streaming tree transducers. In ICALP'12, pages 42--53. Springer, 2012. Google Scholar
Digital Library
- B. S. Baker. Composition of top-down and bottom-up tree transductions. Inform. and Control, 41:186--213, 1979.Google ScholarCross Ref
- O. Becker. Streaming transformations for XML-STX. In R. Eckstein and R. Tolksdorf, editors, XMIDX 2003, volume 24 of LNI, pages 83--88. GI, 2003.Google Scholar
- M. Bojańczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data trees and XML reasoning. In PODS'06, pages 10--19, 2006. Google ScholarDigital Library
- M. Botinčan and D. Babić. Sigma*: symbolic learning of input-output specifications. In POPL'13, pages 443--456, New York, NY, USA, 2013. ACM. Google ScholarDigital Library
- A. Bouajjani, P. Habermehl, L. Holik, T. Touili, and T. Vojnar. Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In CIAA'08, volume 5148 of Lecture Notes in Computer Science, pages 57--67. Springer Berlin Heidelberg, 2008. Google ScholarDigital Library
- M. Brand, J. Heering, P. Klint, and P. Olivier. Compiling Rewrite Systems: The ASF+SDF Compiler. ACM Transactions on Programming Languages and Systems, 24(4), 2002.Google Scholar
- H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications, 2007.Google Scholar
- L. D'Antoni and M. Veanes. Equivalence of extended symbolic finite transducers. In CAV 2013, volume 8044 of LNCS, pages 624--639. Springer, 2013. Google ScholarDigital Library
- L. D'Antoni and M. Veanes. Static analysis of string encoders and decoders. In R. Giacobazzi, J. Berdine, and I. Mastroeni, editors, VMCAI 2013, volume 7737 of LNCS, pages 209--228. Springer, 2013.Google Scholar
- L. D'Antoni and M. Veanes. Minimization of symbolic automata. In S. Jagannathan and P. Sewell, editors, POPL, pages 541--554. ACM, 2014. Google ScholarDigital Library
- L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In TACAS'08, LNCS, 2008. Google ScholarDigital Library
- L. de Moura and N. Bjørner. Satisfiability Modulo Theories: Introduction & Applications. Communications of the ACM, 54(9):69--77, 2011. Google ScholarDigital Library
- J. Engelfriet. Bottom-up and top-down tree transformations -- a comparison. Math. Systems Theory, 9:198--231, 1975.Google ScholarCross Ref
- J. Engelfriet. Top-down tree transducers with regular look-ahead. Math. Systems Theory, 10:289--303, 1977.Google ScholarCross Ref
- J. Engelfriet. Some open questions and recent results on tree transducers and tree languages. In Formal Language Theory, pages 241--286. Academic Press, 1980.Google ScholarCross Ref
- J. Engelfriet and S. Maneth. Macro tree transducers, attribute grammars, and MSO definable tree translations. Inform. and Comput, 154:34--91, 1998. Google ScholarDigital Library
- J. Engelfriet and S. Maneth. The equivalence problem for deterministic MSO tree transducers is decidable. Inf. Process. Lett., 100(5):206--212, Dec. 2006. Google ScholarDigital Library
- T. W. Frühwirth, E. Y. Shapiro, M. Y. Vardi, and E. Yardeni. Logic programs as types for logic programs. In LICS'91, pages 300--309, 1991.Google ScholarCross Ref
- Z. Fülöp and S. Vágvölgyi. Variants of top-down tree transducers with look-ahead. Math. Sys. Th., 21(3):125--145, 1989.Google Scholar
- Z. Fülöp and H. Vogler. Syntax-Directed Semantics: Formal Models Based on Tree Transducers. EATCS. Springer, 1998. Google ScholarDigital Library
- Z. Fülöp and H. Vogler. Forward and backward application of symbolic tree transducers. CoRR, abs/1208.5324, 2012.Google Scholar
- P. Geneves, N. Layaida, and V. Quint. On the analysis of cascading style sheets. In WWW '12, pages 809--818, New York, NY, USA, 2012. ACM. Google ScholarDigital Library
- A. Hejlsberg, S. Wiltamuth, and P. Golde. C# Language Specification. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2003. Google ScholarDigital Library
- P. Hooimeijer, B. Livshits, D. Molnar, P. Saxena, and M. Veanes. Fast and precise sanitizer analysis with Bek. In Proceedings of the USENIX Security Symposium, 2011. Google ScholarDigital Library
- J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Longman Publishing Co., Inc., 1979. Google ScholarDigital Library
- H. Hosoya and B. C. Pierce. Xduce: A statically typed XML processing language. ACM Trans. Internet Technol., 3(2):117--148, May 2003. Google ScholarDigital Library
- N. Kobayashi, N. Tabuchi, and H. Unno. Higher-order multi-parameter tree transducers and recursion schemes for program verification. In POPL'10, pages 495--508, 2010. Google ScholarDigital Library
- A. Kühnemann. Comparison of deforestation techniques for functional programs and for tree transducers. In Fuji Int. Symp. on Functional and Logic Programming, 1999. Google ScholarDigital Library
- O. Lengal, J. Šimáček, and T. Vojnar. Vata: A library for efficient manipulation of non-deterministic tree automata. In TACAS'12, volume 7214 of Lecture Notes in Computer Science, pages 79--94. Springer Berlin Heidelberg, 2012. Google ScholarDigital Library
- A. Maletti, J. Graehl, M. Hopkins, and K. Knight. The power of extended top-down tree transducers. SIAM J. Comput., 39:410--430, June 2009. Google ScholarDigital Library
- S. Maneth, A. Berlea, T. Perst, and H. Seidl. XML type checking with macro tree transducers. In PODS'05, pages 283--294, New York, NY, USA, 2005. ACM. Google ScholarDigital Library
- J. May and K. Knight. A primer on tree automata software for natural language processing, 2008.Google Scholar
- A. Purtee and L. Schubert. TTT: A tree transduction language for syntactic and semantic processing. In Proceedings of the Workshop on App. of Tree Aut. Tech. in NLP, 2012. Google ScholarDigital Library
- J.-C. Raoult. A survey of tree transductions. In Tree Automata and Languages, pages 311--326. sn, 1992.Google Scholar
- H. Seidl. Equivalence of finite-valued tree transducers is decidable. Math. Systems Theory, 27:285--346, 1994. Google ScholarDigital Library
- H. Seidl. Haskell overloading is dexptime-complete. Inf. Process. Lett., 52(2):57--60, 1994. Google ScholarDigital Library
- The Unicode Consortium. The Unicode Standard 6.3, Emoticons. http://unicode.org/charts/PDF/U1F600.pdf.Google Scholar
- M. Veanes and N. Bjørner. Symbolic tree transducers. In Perspectives of System Informatics (PSI'11), volume 7162 of LNCS, pages 377--393. Springer, 2011. Google ScholarDigital Library
- M. Veanes, P. Hooimeijer, B. Livshits, D. Molnar, and N. Bjorner. Symbolic finite state transducers: Algorithms and applications. In POPL'12, 2012. Google ScholarDigital Library
- P. Wadler. Deforestation: transforming programs to eliminate trees. In Proceedings of the Second European Symposium on Programming, pages 231--248, 1988. Google ScholarDigital Library
- P. Walmsley. XQuery. O'Reilly Media, Inc., 2007. Google ScholarDigital Library
Index Terms
- Fast: a transducer-based language for tree manipulation
Recommendations
Fast: A Transducer-Based Language for Tree Manipulation
Tree automata and transducers are used in a wide range of applications in software engineering. While these formalisms are of immense practical use, they can only model finite alphabets. To overcome this problem we augment tree automata and transducers ...
Fast: a transducer-based language for tree manipulation
PLDI '14Tree automata and tree transducers are used in a wide range of applications in software engineering, from XML processing to language type-checking. While these formalisms are of immense practical use, they can only model finite alphabets, and since many ...
About Fast and TReX Accelerations
Fast and TReX tools are designed to analyse systems with infinite state spaces. They both implement algorithms computing the set of reachable states of such systems. Since the state space may be infinite, acceleration techniques are used. In this paper, ...
Comments