---
res:
  bibo_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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Rajeev
      foaf_name: Alur, Rajeev
      foaf_surname: Alur
  - foaf_Person:
      foaf_givenName: Pavol
      foaf_name: Cerny, Pavol
      foaf_surname: Cerny
      foaf_workInfoHomepage: http://www.librecat.org/personId=4DCBEFFE-F248-11E8-B48F-1D18A9856A87
  bibo_doi: 10.1145/1926385.1926454
  bibo_issue: '1'
  bibo_volume: 46
  dct_date: 2011^xs_gYear
  dct_identifier:
  - UT:000289656100050
  dct_language: eng
  dct_publisher: ACM@
  dct_title: Streaming transducers for algorithmic verification of single pass list
    processing programs@
...