Streaming transducers for algorithmic verification of single-pass list processing programs

Date: Thursday, December 16, 2010
Speaker: Pavol Cerny
Venue: TU Wien

We introduce streaming data string transducers that mapinput data strings tooutput data strings in a single left-to-right pass inlinear time. Data strings are (unbounded) sequences ofdata values, tagged with symbols from a finite set, over apotentially infinite data domain that supports onlythe operations of equality and ordering. The transduceruses a finite set of states, a finite set of variablesranging over the data domain, and a finite set ofvariables ranging over data strings. At every step, it canmake decisions based on the next input symbol, updatingits state, remembering the input data value in its datavariables, and updating data-string variables byconcatenating data-string variables and new symbols formedfrom data variables, while avoiding duplication. Weestablish PSPACE bounds for the problems of checkingfunctional equivalence of two streaming transducers, andof checking whether a streaming transducer satisfiespre/post verification conditions specified by streamingacceptors over input/output data-strings.

We identify a class of imperative and a class offunctional programs, manipulating lists of data items,which can be effectively translated to streamingdata-string transducers. The imperative programsdynamically modify a singly-linked heap by changingnext-pointers of heap-nodes and by adding new nodes. Themain restriction specifies how the next-pointers can beused for traversal. We also identify an expressivelyequivalent fragment of functional programs that traverse alist using syntactically restricted recursive calls. Ourresults lead to algorithms for assertion checking and forchecking functional equivalence of two programs, writtenpossibly in different programming styles, for commonlyused routines such as insert, delete, and reverse.

Posted in RiSE Seminar