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 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.
Supplemental Material
- R. Alur and P. Černý. Expressivness of streaming string transducers. Invited paper. In FSTTCS, 2010.Google Scholar
- R. Alur, P. Černý, and S. Weinstein. Algorithmic analysis of array-accessing programs. In CSL, pages 86--101, 2009. Google ScholarDigital Library
- M. Bojańczyk, A. Muscholl, T. Schwentick, L. Segoufin, and C. David. Two-variable logic on words with data. In LICS, pages 7--16, 2006. Google ScholarDigital Library
- A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In CAV, pages 403--418, 2000. Google ScholarDigital Library
- A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying programs with dynamic 1-selector-linked structures in regular model checking. In TACAS, pages 13--29, 2005. Google ScholarDigital Library
- A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. In CAV, pages 517--531, 2006. Google ScholarDigital Library
- M. Bozga and R. Iosif. On flat programs with lists. In VMCAI, pages 122--136, 2007. Google ScholarDigital Library
- P. Černý, A. Radhakrishna, D. Zufferey, S. Chaudhuri, and R. Alur. Model checking of linearizability of concurrent list implementations. In CAV, pages 465--479, 2010. Google ScholarDigital Library
- S. Chakraborty. Reasoning about heap manipulating programs using automata techniques. To appear in IISc-World Scientific Review Volume on Modern Applications of Automata Theory.Google Scholar
- D. Distefano, P. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS, pages 287--302, 2006. Google ScholarDigital Library
- J. Engelfriet and H. Hoogeboom. MSO definable string transductions and two-way finite-state transducers. ACM Trans. Comput. Log., 2 (2): 216--254, 2001. Google ScholarDigital Library
- W. Landi. Undecidability of static analysis. LOPLAS, 1 (4): 323--337, 1992. Google ScholarDigital Library
- R. Manevich, E. Yahav, G. Ramalingam, and S. Sagiv. Predicate abstraction and canonical abstraction for singly-linked lists. In VMCAI, pages 181--198, 2005. Google ScholarDigital Library
- R. Manevich, J. Berdine, B. Cook, G. Ramalingam, and M. Sagiv. Shape analysis by graph decomposition. In TACAS, pages 3--18, 2007. Google ScholarDigital Library
- F. Neven, T. Schwentick, and V. Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic, 5 (3): 403--435, 2004. Google ScholarDigital Library
- B. Pierce. Types and programming languages. MIT Press, 2002. Google ScholarDigital Library
- A. Podelski and T. Wies. Counterexample-guided focus. In POPL, pages 249--260, 2010. Google ScholarDigital Library
- G. Ramalingam. The undecidability of aliasing. ACM Trans. Program. Lang. Syst., 16 (5): 1467--1471, 1994. Google ScholarDigital Library
- S. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst., 24 (3): 217--298, 2002. Google ScholarDigital Library
- T. Touili. Regular model checking using widening techniques. Electr. Notes Theor. Comput. Sci., 50 (4), 2001.Google Scholar
Index Terms
- Streaming transducers for algorithmic verification of single-pass list-processing programs
Recommendations
Streaming transducers for algorithmic verification of single-pass list-processing programs
POPL '11We 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 ...
Copyful Streaming String Transducers
Special Issue on the 11th International Workshop on Reachability Problems (RP 2017)Copyless streaming string transducers (copyless SST) have been introduced by R. Alur and P. Černý in 2010 as a one-way deterministic automata model to define transductions of finite strings. Copyless SST extend deterministic finite state automata with a ...
Algorithmic analysis of array-accessing programs
For programs whose data variables range over Boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this article, we consider algorithmic verification of programs that use ...
Comments