Summary
Symbolic finite state transducers (SFSTs) provide a precise model for reasoning about string-manipulating programs, but existing approaches are limited in their ability to handle the complexity and scale of real-world string operations. We extend the Bek framework with support for data-parallel string-manipulating programs, introducing a formalism that combines SFSTs with an expressive algebra for data-parallel operations. Our extended framework can model a broader class of string manipulation functions, including those involving regular expression matching, parsing, and internationalization. We provide decision procedures for composition and equivalence checking of the extended transducers, and evaluate the approach on a corpus of real-world JavaScript string operations.