Loris D'antoni
Margus Veanes
Benjamin Livshits
Skip Abstract Section
Abstract
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 with symbolic alphabets represented as parametric theories. Admitting infinite alphabets makes these models more general and succinct than their classic 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 preceding formalisms.
- Rajeev Alur and Loris D’Antoni. 2012. Streaming tree transducers. In Automata, Languages, and Programming, Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer (Eds.). Lecture Notes in Computer Science, Vol. 7392. Springer, Berlin, 42--53. DOI:http://dx.doi.org/10.1007/978-3-642-31585-5_8 Google Scholar
Digital Library
- Brenda S. Baker. 1979. Composition of top-down and bottom-up tree transductions. Inform. Control 41, 2 (1979), 186--213.Google ScholarCross Ref
- Oliver Becker. 2003. Streaming transformations for XML-STX. In XMIDX 2003 (LNI), Rainer Eckstein and Robert Tolksdorf (Eds.), Vol. 24. GI, 83--88.Google Scholar
- Mikolaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. 2006. Two-variable logic on data trees and XML reasoning. In Proceedings of the 25th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS’06). ACM, New York, NY, 10--19. DOI:http://dx.doi.org/10.1145/1142351.1142354 Google ScholarDigital Library
- Matko Botinčan and Domagoj Babić. 2013. Sigma*: Symbolic learning of input-output specifications. SIGPLAN Not. 48, 1 (Jan. 2013), 443--456. DOI:http://dx.doi.org/10.1145/2480359.2429123 Google ScholarDigital Library
- Ahmed Bouajjani, Peter Habermehl, Lukas Holik, Tayssir Touili, and Tomas Vojnar. 2008. Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In CIAA’08. Lecture Notes in Computer Science, Vol. 5148. Springer, Berlin, 57--67. DOI:http://dx.doi.org/10.1007/978-3-540-70844-5_7 Google ScholarDigital Library
- Hubert Comon, Max Dauchet, Remi Gilleron, Christof Löding, Florent Jacquemard, Denis Lugiez, Sophie Tison, and Marc Tommasi. 2007. Tree Automata Techniques and Applications.Google Scholar
- Conrad Cotton-Barratt, David Hopkins, Andrzej S. Murawski, and C.-H. Luke Ong. 2015. Fragments of ML decidable by nested data class memory automata. In Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015. Proceedings. 249--263. DOI:http://dx.doi.org/10.1007/978-3-662-46678-0_16Google ScholarCross Ref
- Loris D’Antoni and Margus Veanes. 2013a. Equivalence of extended symbolic finite transducers. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV’13). Springer-Verlag, Berlin, 624--639. DOI:http://dx.doi.org/10.1007/978-3-642-39799-8_41 Google ScholarDigital Library
- Loris D’Antoni and Margus Veanes. 2013b. Static analysis of string encoders and decoders. In VMCAI 2013 (LNCS), R. Giacobazzi, J. Berdine, and I. Mastroeni (Eds.), Vol. 7737. Springer, 209--228.Google ScholarDigital Library
- Loris D’Antoni and Margus Veanes. 2014. Minimization of symbolic automata. In POPL, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 541--554. Google ScholarDigital Library
- Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, 337--340. http://dl.acm.org/citation.cfm?id=1792734.1792766 Google ScholarDigital Library
- Leonardo de Moura and Nikolaj Bjørner. 2011. Satisfiability modulo theories: Introduction & applications. Commun. ACM 54, 9 (2011), 69--77. Google ScholarDigital Library
- Joost Engelfriet. 1975. Bottom-up and top-down tree transformations—A comparison. Math. Syst. Theory 9 (1975), 198--231.Google ScholarCross Ref
- Joost Engelfriet. 1977. Top-down tree transducers with regular look-ahead. Math. Syst. Theory 10 (1977), 289--303.Google ScholarCross Ref
- Joost Engelfriet. 1980. Some open questions and recent results on tree transducers and tree languages. In Formal Language Theory. Academic Press, 241--286.Google Scholar
- Joost Engelfriet and Sebastian Maneth. 2006. The equivalence problem for deterministic MSO tree transducers is decidable. Inf. Process. Lett. 100, 5 (Dec. 2006), 206--212. DOI:http://dx.doi.org/10.1016/j.ipl.2006.05.015 Google ScholarDigital Library
- Joost Engelfriet and Heiko Vogler. 1985. Macro tree transducers. J. Comput. Syst. Sci. 31 (1985), 71--146.Google ScholarCross Ref
- Z. Esik. 1980. Decidability results concerning tree transducers. Acta Cybern. 5 (1980), 1--20.Google Scholar
- Thom W. Frühwirth, Ehud Y. Shapiro, Moshe Y. Vardi, and Eyal Yardeni. 1991. Logic programs as types for logic programs. In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS ’91). 300--309. DOI:http://dx.doi.org/10.1109/LICS.1991.151654Google ScholarCross Ref
- Zoltán Fülöp and Sándor Vágvölgyi. 1989. Variants of top-down tree transducers with look-ahead. Math. Syst. Theory 21, 3 (1989), 125--145.Google ScholarDigital Library
- Zoltán Fülöp and Heiko Vogler. 2014. Forward and backward application of symbolic tree transducers. Acta Inf. 51, 5 (Aug. 2014), 297--325. DOI:http://dx.doi.org/10.1007/s00236-014-0197-7 Google ScholarDigital Library
- Zoltán Fülöp and H. Vogler. 1998. Syntax-Directed Semantics: Formal Models Based on Tree Transducers. Springer. Google ScholarDigital Library
- Pierre Geneves, Nabil Layaida, and Vincent Quint. 2012. On the analysis of cascading style sheets. In WWW’12. ACM, New York, NY, 809--818. DOI:http://dx.doi.org/10.1145/2187836.2187946 Google ScholarDigital Library
- Shizuya Hakuta, Sebastian Maneth, Keisuke Nakano, and Hideya Iwasaki. 2014. XQuery streaming by forest transducers. In IEEE 30th International Conference on Data Engineering (ICDE’14). 952--963. DOI:http://dx.doi.org/10.1109/ICDE.2014.6816714Google ScholarCross Ref
- Anders Hejlsberg, Scott Wiltamuth, and Peter Golde. 2003. C# Language Specification. Addison-Wesley Longman Publishing Co., Inc., Boston, MA. Google ScholarDigital Library
- Pieter Hooimeijer, Benjamin Livshits, David Molnar, Prateek Saxena, and Margus Veanes. 2011. Fast and precise sanitizer analysis with BEK. In Proceedings of the 20th USENIX Conference on Security (SEC’11). USENIX Association, Berkeley, CA, 1--1. Google ScholarDigital Library
- John E. Hopcroft and Jeffrey D. Ullman. 1979. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Longman Publishing Co., Inc. Google ScholarDigital Library
- Haruo Hosoya and Benjamin C. Pierce. 2003. XDuce: A statically typed XML processing language. ACM Trans. Internet Technol. 3, 2 (May 2003), 117--148. DOI:http://dx.doi.org/10.1145/767193.767195 Google ScholarDigital Library
- Naoki Kobayashi, Naoshi Tabuchi, and Hiroshi Unno. 2010. Higher-order multi-parameter tree transducers and recursion schemes for program verification. SIGPLAN Not. 45, 1 (Jan. 2010), 495--508. DOI:http://dx.doi.org/10.1145/1707801.1706355 Google ScholarDigital Library
- Armin Kühnemann. 1999. Comparison of deforestation techniques for functional programs and for tree transducers. In Proceedings of the 4th Fuji International Symposium on Functional and Logic Programming. Google ScholarDigital Library
- Ond Lengal, Ji Simáček, and Tom Vojnar. 2012. VATA: A library for efficient manipulation of non-deterministic tree automata. In TACAS’12. Lecture Notes in Computer Science, Vol. 7214. Springer, Berlin, 79--94. DOI:http://dx.doi.org/10.1007/978-3-642-28756-5_7 Google ScholarDigital Library
- Andreas Maletti, Jonathan Graehl, Mark Hopkins, and Kevin Knight. 2009. The power of extended top-down tree transducers. SIAM J. Comput. 39, 2 (June 2009), 410--430. Google ScholarDigital Library
- Sebastian Maneth, Alexandru Berlea, Thomas Perst, and Helmut Seidl. 2005. XML type checking with macro tree transducers. In PODS’05. ACM, New York, NY, 283--294. DOI:http://dx.doi.org/10.1145/1065167.1065203 Google ScholarDigital Library
- Jonathan May and Kevin Knight. 2008. A Primer on Tree Automata Software for Natural Language Processing. http://www.isi.edu/licensed-sw/tiburon/tiburon-tutorial.pdf.Google Scholar
- Tova Milo, Dan Suciu, and Victor Vianu. 2000. Typechecking for XML transformers. In Proceedings of the 19th ACM Symposium on Principles of Database Systems (PODS’00). ACM, 11--22. Google ScholarDigital Library
- Thomas Perst and Helmut Seidl. 2004. Macro forest transducers. Inf. Process. Lett. 89, 3 (Feb. 2004), 141--149. DOI:http://dx.doi.org/10.1016/j.ipl.2003.05.001 Google ScholarDigital Library
- Adam Purtee and Lenhart Schubert. 2012. TTT: A tree transduction language for syntactic and semantic processing. In Proceedings of the Workshop on Application of Tree Automata Techniques in NLP. Google ScholarDigital Library
- Jean-Claude Raoult. 1992. A survey of tree transductions. In Tree Automata and Languages., 311--326.Google Scholar
- Helmut Seidl. 1994a. Equivalence of finite-valued tree transducers is decidable. Math. Syst. Theory 27 (1994), 285--346. Google ScholarDigital Library
- Helmut Seidl. 1994b. Haskell overloading is DEXPTIME-complete. Inf. Process. Lett. 52, 2 (1994), 57--60. Google ScholarDigital Library
- The Unicode Consortium. The Unicode Standard 6.3, Emoticons. The Unicode Consortium. http://unicode.org/charts/PDF/U1F600.pdf.Google Scholar
- Mark G. J. van den Brand, J. Heering, P. Klint, and P. A. Olivier. 2002. Compiling language definitions: The ASF+SDF compiler. ACM Trans. Program. Lang. Syst. 24, 4 (July 2002), 334--368. DOI:http://dx.doi.org/10.1145/567097.567099 Google ScholarDigital Library
- Margus Veanes and Nikolaj Bjørner. 2012. Symbolic tree transducers. In Proceedings of the 8th International Conference on Perspectives of System Informatics (PS’11). Springer-Verlag, Berlin, 377--393. DOI:http://dx.doi.org/10.1007/978-3-642-29709-0_32 Google ScholarDigital Library
- Margus Veanes and Nikolaj Bjørner. 2015. Symbolic tree automata. Inform. Process. Lett. 115, 3 (2015), 418--424. DOI:http://dx.doi.org/10.1016/j.ipl.2014.11.005Google ScholarCross Ref
- Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjørner. 2012. Symbolic finite state transducers: Algorithms and applications. SIGPLAN Not. 47, 1 (Jan. 2012), 137--150. DOI:http://dx.doi.org/10.1145/2103621.2103674 Google ScholarDigital Library
- Philip Wadler. 1988. Deforestation: Transforming programs to eliminate trees. Theor. Comput. Sci. 73, 2 (Jan. 1988), 231--248. DOI:http://dx.doi.org/10.1016/0304-3975(90)90147-A Google ScholarDigital Library
- Priscilla Walmsley. 2007. XQuery. O’Reilly Media, Inc. Google ScholarDigital Library
Index Terms
- Fast: A Transducer-Based Language for Tree Manipulation
Recommendations
Fast: a transducer-based language for tree manipulation
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and ImplementationTree 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 ...
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