---
_id: '3325'
abstract:
- lang: eng
  text: 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.
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Pavol
  full_name: Cerny, Pavol
  id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
  last_name: Cerny
citation:
  ama: 'Alur R, Cerny P. Streaming transducers for algorithmic verification of single
    pass list processing programs. In: Vol 46. ACM; 2011:599-610. doi:<a href="https://doi.org/10.1145/1926385.1926454">10.1145/1926385.1926454</a>'
  apa: 'Alur, R., &#38; Cerny, P. (2011). Streaming transducers for algorithmic verification
    of single pass list processing programs (Vol. 46, pp. 599–610). Presented at the
    POPL: Principles of Programming Languages, Texas, USA: ACM. <a href="https://doi.org/10.1145/1926385.1926454">https://doi.org/10.1145/1926385.1926454</a>'
  chicago: Alur, Rajeev, and Pavol Cerny. “Streaming Transducers for Algorithmic Verification
    of Single Pass List Processing Programs,” 46:599–610. ACM, 2011. <a href="https://doi.org/10.1145/1926385.1926454">https://doi.org/10.1145/1926385.1926454</a>.
  ieee: 'R. Alur and P. Cerny, “Streaming transducers for algorithmic verification
    of single pass list processing programs,” presented at the POPL: Principles of
    Programming Languages, Texas, USA, 2011, vol. 46, no. 1, pp. 599–610.'
  ista: 'Alur R, Cerny P. 2011. Streaming transducers for algorithmic verification
    of single pass list processing programs. POPL: Principles of Programming Languages
    vol. 46, 599–610.'
  mla: Alur, Rajeev, and Pavol Cerny. <i>Streaming Transducers for Algorithmic Verification
    of Single Pass List Processing Programs</i>. Vol. 46, no. 1, ACM, 2011, pp. 599–610,
    doi:<a href="https://doi.org/10.1145/1926385.1926454">10.1145/1926385.1926454</a>.
  short: R. Alur, P. Cerny, in:, ACM, 2011, pp. 599–610.
conference:
  end_date: 2011-01-28
  location: Texas, USA
  name: 'POPL: Principles of Programming Languages'
  start_date: 2011-01-26
date_created: 2018-12-11T12:02:41Z
date_published: 2011-01-26T00:00:00Z
date_updated: 2025-09-30T09:10:38Z
day: '26'
department:
- _id: ToHe
doi: 10.1145/1926385.1926454
external_id:
  isi:
  - '000289656100050'
intvolume: '        46'
isi: 1
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 599 - 610
publication_status: published
publisher: ACM
publist_id: '3310'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Streaming transducers for algorithmic verification of single pass list processing
  programs
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 46
year: '2011'
...