Problem
Finite automata and ?nite transducers are used in a wide range of applications in software engineering, from regular expressions to speci?cation languages. We extend these classic objects with symbolic alphabets represented as parametric theories. Admitting potentially in?nite alphabets makes this representation strictly more general and succinct than classical ?nite transducers and automata over strings.
Approach
Despite this, the main operations, including composition, checking that a transducer is single-valued, and equivalence checking for single-valued symbolic ?nite transducers are effective given a decision procedure for the background theory. We provide novel algorithms for these operations and extend composition to symbolic transducers augmented with registers. Our base algorithms are unusual in that they are nonconstructive, therefore, we also supply a separate model generation algorithm that can quickly find counterexamples in the case two symbolic ?nite transducers are not equivalent.
Results
The algorithms give rise to a complete decidable algebra of symbolic transducers. Unlike previous work, we do not need any syntactic restriction of the formulas on the transitions, only a decision procedure. In practice we leverage recent advances in satis?ability modulo theory (SMT) solvers. We demonstrate our techniques on four case studies, covering a wide range of applications. Our techniques can synthesize string pre-images in excess of 8, 000 bytes in roughly a minute, and we ?nd that our new encodings signi?cantly outperform previous techniques in succinctness and speed of analysis.