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

DOI10.1145/1926385.1926454zbMATH Open1284.68159arXiv1007.4958OpenAlexW4251691259MaRDI QIDQ5408580FDOQ5408580

Authors: Pavol Černý, Rajeev Alur 

Publication date: 10 April 2014

Published in: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

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 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 input/output data-strings, are in PSPACE. 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.

Full work available at URL: https://arxiv.org/abs/1007.4958

Recommendations

• Expressiveness of streaming string transducers
• Nondeterministic Streaming String Transducers
• Streaming ranked-tree-to-string transducers

zbMATH Keywords

transducerslistsalgorithmic software verification

Mathematics Subject Classification ID

Data structures (68P05) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cited In (30)

• Copyless cost-register automata: structure, expressiveness, and closure properties
• Better complexity bounds for cost register automata
• Better complexity bounds for cost register automata
• On bidirectional runtime enforcement
• Pattern eliminating transformations
• Regular Programming for Quantitative Properties of Data Streams
• Foundations of Boolean stream runtime verification
• On runtime enforcement via suppressions
• Non-deterministic transducer models of retransmission protocols over noisy channels
• Streaming ranked-tree-to-string transducers
• Extended symbolic finite automata and transducers
• Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
• On the Model Checking Problem for Some Extension of CTL*
• Semantic Foundations for Deterministic Dataflow and Stream Processing
• Copyful streaming string transducers
• Equivalence checking problem for finite state transducers over semigroups
• String-to-string interpretations with polynomial-size output
• Streaming Property Testing of Visibly Pushdown Languages *
• Simple linear string constraints
• Streamable regular transductions
• Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines
• On first-order runtime enforcement of branching-time properties
• Reasoning on data words over numeric domains
• Expressiveness of streaming string transducers
• Nondeterministic Streaming String Transducers
• Sequentiality of string-to-context transducers
• An automata-theoretic approach to the verification of distributed algorithms
• Title not available (Why is that?)
• Regular Transformations of Data Words Through Origin Information
• Complexity of regular functions

This page was built for publication: Streaming transducers for algorithmic verification of single-pass list-processing programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408580)