  This paper proposes relational program synthesis, a new problem that concerns
synthesizing one or more programs that collectively satisfy a relational
specification. As a dual of relational program verification, relational program
synthesis is an important problem that has many practical applications, such as
automated program inversion and automatic generation of comparators. However,
this relational synthesis problem introduces new challenges over its
non-relational counterpart due to the combinatorially larger search space. As a
first step towards solving this problem, this paper presents a synthesis
technique that combines the counterexample-guided inductive synthesis framework
with a novel inductive synthesis algorithm that is based on relational version
space learning. We have implemented the proposed technique in a framework
called Relish, which can be instantiated to different application domains by
providing a suitable domain-specific language and the relevant relational
specification. We have used the Relish framework to build relational
synthesizers to automatically generate string encoders/decoders as well as
comparators, and we evaluate our tool on several benchmarks taken from prior
work and online forums. Our experimental results show that the proposed
technique can solve almost all of these benchmarks and that it significantly
outperforms EUSolver, a generic synthesis framework that won the general track
of the most recent SyGuS competition.
