**Monday, January 24, 2011**

### Levine 612, 1:30 p.m. - 3:00 p.m.

Pavol Cerny

IST Austria

Streaming Transducers for Algorithmic Verification of Single-pass List-processing Programs

*Abstract:*
We introduce streaming data string transducers that map input data
strings to output data strings in a single left-to-right pass in linear
time. Data strings are (unbounded) sequences of data values, tagged with
symbols from a finite set, over a potentially infinite data domain that
supports only the operations of equality and ordering. The transducer
uses a finite set of states, a finite set of variables ranging over the
data domain, and a finite set of variables ranging over data strings.
At every step, it can make decisions based on the next input symbol,
updating its state, remembering the input data value in its data
variables, and updating data-string variables by concatenating
data-string variables and new symbols formed from data variables, while
avoiding duplication. We establish that the problems of checking
functional equivalence of two streaming transducers, and of checking
whether a streaming transducer satisfies pre/post verification
conditions specified by streaming acceptors over input/output
data-strings, are in PSPACE.
We identify a class of imperative and a class of functional programs,
manipulating lists of data items, which can be effectively translated to
streaming data-string transducers. The imperative programs dynamically
modify a singly-linked heap by changing next-pointers of heap-nodes and
by adding new nodes. The main restriction specifies how the
next-pointers can be used for traversal. We also identify an
expressively equivalent fragment of functional programs that traverse a
list using syntactically restricted recursive calls. Our results lead to
algorithms for assertion checking and for checking functional
equivalence of two programs, written possibly in different programming
styles, for commonly used routines such as insert, delete, and reverse.

*Bio:*