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

DOI10.1145/1926385.1926454MaRDI QIDQ5408580zbMATH OpenOpenAlexFDO

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)

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

zbMATH Keywords

algorithmic software verificationliststransducers

Mathematics Subject Classification ID

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

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.

Recommendations

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

Cited in

(34)

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

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)