Fast: A transducer-based language for tree manipulation

Tree automata and tree transducers are used in a wide range of applications in software engineering, from XML process-ing to language type-checking. While these formalisms are of immense practical use, they can only model finite alpha-bets, 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 para-metric theories. Admitting infinite alphabets makes these models more general and succinct than their classical coun-terparts. Despite this, we show how the main operations, such as composition and language equivalence, remain com-putable 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 sym-bolic alphabets through tight integration with state-of-the-art satisfiability modulo theory (SMT) solvers. We demon-strate our techniques on practical case studies, covering a wide range of applications