Synthesizing Transducers from Complex Specifications

TL;DR

This paper introduces a formal, constraint-based method for synthesizing transducers from complex specifications, enabling more reliable and modifiable string transformation programs with applications in verification and repair.

Contribution

It presents the first approach to synthesize transducers from complex specifications using SMT solvers, leveraging their formal properties for improved flexibility and correctness.

Findings

Supports input-output examples, types, and distances specifications

Uses transducer properties to generate solvable constraints

Enables repair of partially correct transducers

Abstract

Automating string transformations has been one of the killer applications of program synthesis. Existing synthesizers that solve this problem produce programs in domain-specific languages (DSL) that are engineered to help the synthesizer, and therefore lack nice formal properties. This limitation prevents the synthesized programs from being used in verification applications (e.g., to check complex pre-post conditions) and makes the synthesizers hard to modify due to their reliance on the given DSL. We present a constraint-based approach to synthesizing transducers, a well-studied model with strong closure and decidability properties. Our approach handles three types of specifications: (i) input-output examples, (ii) input-output types expressed as regular languages, and (iii) input/output distances that bound how many characters the transducer can modify when processing an input string. Our work is the first to support such complex specifications and it does so by using the algorithmic properties of transducers to generate constraints that can be solved using off-the-shelf SMT solvers. Our synthesis approach can be extended to many transducer models and it can be used, thanks to closure properties of transducers, to compute repairs for partially correct transducers.