Loris D'Antoni, Margus Veanes, Benjamin Livshits, and David Molnar
We introduce a tree manipulation language, FAST, that overcomes technical limitations of previous tree manipulation languages, such as XPath and XSLT which do not support precise program analysis, or TTT and Tiburon which only support trees over finite alphabets. At the heart of FAST is a combination of SMT solvers and tree transducers, enabling it to model programs whose input and output can range over any decidable theory. The language can express multiple applications. We write an HTML ``sanitizer" in FAST and obtain results comparable to leading libraries but with smaller code. Next we show how augmented reality ``tagging" applications can be checked for potential overlap in milliseconds using FAST type checking. We show how transducer composition enables deforestation for improved performance. Overall, we strike a balance between expressiveness and precise analysis that works for a large class of important tree-manipulating programs.