Programming using automata and transducers / D'Antoni, Loris.

Format:

Book

Thesis/Dissertation

Author/Creator:

D'Antoni, Loris, author.

Contributor:

Alur, Rajeev, 1966- degree supervisor.

Veanes, Margus, degree committee member.

Tannen, Val, 1953- degree committee member.

Pierce, Benjamin C., degree committee member.

Kannan, Sampath, degree committee member.

University of Pennsylvania. Computer and Information Science, degree granting institution.

Language:

English

Subjects (All):

Computer science.

0984.

Local Subjects:

Computer science.

0984.

Genre:

Academic theses.

Physical Description:

1 electronic resource (213 pages)

Contained In:

Dissertation Abstracts International 77-01B(E).

Place of Publication:

Ann Arbor : ProQuest Dissertations & Theses, 2015.

Language Note:

English

Summary:

Automata, the simplest model of computation, have proven to be an effective tool in reasoning about programs that operate over strings. Transducers augment automata to produce outputs and have been used to model string and tree transformations such as natural language translations. The success of these models is primarily due to their closure properties and decidable procedures, but good properties come at the price of limited expressiveness. Concretely, most models only support finite alphabets and can only represent small classes of languages and transformations.

We focus on addressing these limitations and bridge the gap between the theory of automata and transducers and complex real-world applications: Can we extend automata and transducer models to operate over structured and infinite alphabets? Can we design languages that hide the complexity of these formalisms? Can we define executable models that can process the input efficiently? .

First, we introduce succinct models of transducers that can operate over large alphabets and design BEX, a language for analysing string coders. We use BEX to prove the correctness of UTF and B ASE64 encoders and decoders. Next, we develop a theory of tree transducers over infinite alphabets and design FAST, a language for analysing tree-manipulating programs. We use FAST to detect vulnerabilities in HTML sanitizers, check whether augmented reality taggers conflict, and optimize and analyze functional programs that operate over lists and trees. Finally, we focus on laying the foundations of stream processing of hierarchical data such as XML files and program traces. We introduce two new efficient and executable models that can process the input in a left-to-right linear pass: symbolic visibly pushdown automata and streaming tree transducers. Symbolic visibly pushdown automata are closed under Boolean operations and can specify and efficiently monitor complex properties for hierarchical structures over infinite alphabets. Streaming tree transducers can express and efficiently process complex XML transformations while enjoying decidable procedures.

Notes:

Source: Dissertation Abstracts International, Volume: 77-01(E), Section: B.

Advisors: Rajeev Alur Committee members: Sampath Kannan; Benjamin C. Pierce; Val Tannen; Margus Veanes.

Ph.D. University of Pennsylvania 2015.

Local Notes:

School code: 0175

ISBN:

9781339030593