Streaming transducers for algorithmic verification of single pass list processing programs Conference Paper

Author(s): Alur, Rajeev; Cerný, Pavol
Title: Streaming transducers for algorithmic verification of single pass list processing programs
Affiliation IST Austria
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 do- main 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 in- put symbol, updating its state, remembering the input data value in its data variables, and updating data-string variables by concatenat- ing data-string variables and new symbols formed from data vari- ables, 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 in- put/output data-strings, are in PSPACE. We identify a class of imperative and a class of functional pro- grams, manipulating lists of data items, which can be effectively translated to streaming data-string transducers. The imperative pro- grams dynamically modify a singly-linked heap by changing next- pointers of heap-nodes and by adding new nodes. The main re- striction 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.
Conference Title: POPL: Principles of Programming Languages
Publisher: ACM  
Date Published: 2011-01-24
Start Page: 599
End Page: 610
Sponsor: This research was partially supported by NSF grants CCF 0915777 and CCF 0905464.
DOI: 10.1145/1926385.1926454
Open access: no
IST Austria Authors
  1. Pavol Černý
    25 Cerný
Related IST Austria Work