View article

Given a specification and a set of candidate programs (program space), the program synthesis problem is to find a candidate program that satisfies the specification. We present the synthesis through unification (STUN) approach, which is an extension of the counter-example guided inductive synthesis (CEGIS) approach. In CEGIS, the synthesizer maintains a subset S of inputs and a candidate program that is correct for S. The synthesizer repeatedly checks if there exists a counterexample input c such that the execution of is incorrect on c. If so, the synthesizer enlarges S to include c, and picks a program from the program space that is correct for the new set S.

The STUN approach extends CEGIS with the idea that given a program that is correct for a subset of inputs, the synthesizer can try to find a program that is correct for the rest of the inputs. If and can be unified into a …