Transducers are a natural automata-based formal model for synthesizing string transformations.
A finite state transducer (FT) is an automaton where each transition reads an input
character and outputs a string of output characters.
For instance, Figure REF  shows a transducer that `escapes' instances of the " character.
So, on input a"\"a, the transducer outputs the string a\"\\"a.
FTs have found wide adoption in a variety of domains [1]}, [2]} because of their many desirable properties (e.g., decidable equivalence check and closure under composition [3]}).
There has been increasing work on building SMT solvers for strings that support transducers; the Ostrich tool [4]} allows a user to write programs in SMT where string-transformations are modelled using transducers.
One can then write constraints over such programs and use an SMT solver to automatically check for satisfiability or prove unsatisfiability of those constraints.
For example, given a program like the following:
