Techniques for verifying string transformations rely on automata-theoretic approaches that provide powerful decidability properties [1]}.
On the other hand, techniques for synthesizing string transformations rely on domain-specific languages (DSLs) [2]}, [3]}.
These DSLs are designed to make synthesis practical and have to give up the closure and decidability properties enabled by automata-theoretic models.
The disconnect between the two approaches raises a natural question: Can one synthesize automata-based models and therefore retain and leverage their elegant properties?
