Problem
1 Fast: A Transducer-Based Language for Tree Manipulation LORIS D’ANTONI, University of Pennsylvania MARGUS VEANES, BENJAMIN LIVSHITS, and DAVID MOLNAR, Microsoft Research 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.
Approach
Categories and Subject Descriptors: F.1.1 [Theory of Computation]: Models of Computation, Automata General Terms: Algorithms, Languages, Verification Additional Key Words and Phrases: Symbolic tree transducers, FAST ACM Reference Format: Loris D’Antoni, Margus Veanes, Benjamin Livshits, and David Molnar. 2015. Fast: A transducer-based language for tree manipulation. ACM Trans. Program. Lang.
Results
Syst. 38, 1, Article 1 (October 2015), 32 pages. DOI: http://dx.doi.org/10.1145/2791292 1. INTRODUCTION This article introduces Functional Abstraction of Symbolic Transducers (FAST), a new language for analyzing and modeling programs that manipulate trees over potentially infinite domains. FAST builds on top of satisfiability modulo theory solvers, tree au- tomata, and tree transducers. Tree automata are used in a variety of applications in software engineering, from analysis of XML programs [Hosoya and Pierce 2003] to language type checking [Seidl 1994b]. Tree transducers extend tree automata to model functions over trees, and appear in fields such as natural language processing [Maletti et al. 2009; Purtee and Schubert 2012; May and Knight 20