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

Streaming transducers for algorithmic verification of single-pass list-processing programs,10.1145/1925844.1926454,Sigplan Notices,Rajeev Alur,Pavol Č

Streaming transducers for algorithmic verification of single-pass list-processing programs   (Citations: 5)
BibTex | RIS | RefWorks Download
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 PSPACE bounds for 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. 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.
Journal: Sigplan Notices - SIGPLAN , pp. 599-610, 2011
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...For example, to pairwise add the numbers in two sequences we could use zipwith(+; [0; 1; 2]; [3; 4; 5]) = [3; 5; 7],Streaming transducers [1] provide another recent symbolic extension of nite transducers where the label theories are restricted to be total orders, in order to maintain decidability of equivalence...

    Margus Veaneset al. Data-Parallel String-Manipulating Programs

    • ...Streaming transducers [1] provide another recent symbolic extension of finite transducers where the label theories are restricted to be total orders...

    Margus Veaneset al. Symbolic Tree Transducers

    • ...Streaming transducers [1] provide another recent symbolic extension of finite transducers where the label theories are restricted to be total orders, in order to maintain decidability of equivalence...

    Margus Veaneset al. Generating Fast String Manipulating Code Through Transducer Exploratio...

    • ...This talk is based on results reported in [2] and [1]...

    Rajeev Alur. Streaming String Transducers

    • ...Deterministic streaming string transducers (dssts), first introduced in [1,2], in addition to all transductions implemented by deterministic finite transducers, can implement transductions such as reversing a string and swapping substrings...
    • ...Deterministic streaming string transducers (dsst) have been proposed as an effective machine model for MSO-definable string transductions [2,1]...
    • ...Let T1 be a( Σ1 ,Σ 2)-dsst, with the set of states Q1, and the set of string variables X1, and let T2 be a (Σ2 ,Σ 3)-dsst with the set of states Q2 and the set of string variables X2. We review the construction from [1] to construct the (Σ1 ,Σ 3)dsst Ts = T1 ◦ T2, i.e., Ts is the sequential composition of T1 and T2 .L et the set of states and the set of string variables of Ts be Qs and Xs respectively...
    • ...The following relationships are known: dmsos = 2dgsm [6], dmsos = dsst [1], nmsos � 2ngsm and 2ngsm � nmsos [6]...
    • ...We first show that for every nsst T we can define a nmsos transduction W such that T = W .I n [1], the authors shows how a sequence of states and copyless assignments of a dsst can be encoded in the copy set of a dmsos-transduction...
    • ...The construction for part (a) is as discussed, for details see [1]...
    • ...state q, one string variable x ,a nd for alla ∈ Σ, its transitions are of the form (q, a, x := x.γ, q), where γ is a finite string in Γ ∗ .F rom [1], we know that for...

    Rajeev Aluret al. Nondeterministic Streaming String Transducers

Sort by: