In Proceedings of the ACM Conference on Programmin
In Proceedings of the ACM Conference on Programming Languages Design and Implementation (PLDI) 2014 Year 2014 Peer-reviewed
BibTeX PDF
Programming Languages · Static Analysis

Fast: a Transducer-Based Language for Tree Manipulation

Loris D'Antoni Margus Veanes Benjamin Livshits David Molnar
CCS
Venue
Peer-reviewed
Type
2014
Publication year
§ Abstract

Problem

Tree automata and tree transducers are used in a wide range of applications in software engineering, from natural language processing to language type-checking. While these formalisms are of immense practical use, they can only model finite input alphabets. However, many real-world applications operate over infinite domains, such as integers.

Approach

To overcome this limitation 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.

Results

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.

Cite this paper — BibTeX 
@InProceedings{fast2014,
  author ={Loris D'Antoni and Margus Veanes and Benjamin Livshits and David Molnar},
  title ={Fast: a Transducer-Based Language for Tree Manipulation},
  MONTH = June,
  YEAR = 2014,
  BOOKTITLE = {In Proceedings of the ACM Conference on Programming Languages Design and Implementation (PLDI) 2014}
}
Copied