**Date: **
17:00,
Wednesday, June 3, 2015

**Speaker: **
Arjun Radhakrishna

**Venue: **IST Austria

**Notes: **

**Day: Wednesday**

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 P

that is correct for S. The synthesizer repeatedly checks if there exists

a counterexample input c such that the execution of P 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 P

that is correct for a subset S of inputs, the synthesizer can try to

find a program P’ that is correct for the rest of the inputs. If P and

P’ can be unified into a program in the program space, then a solution

has been found. We present a generic synthesis procedure based on the

STUN approach and specialize it for two different domains (linear

arithmetic and bitvectors) by providing the appropriate unification

operators. We implemented these specializations in a prototype tool, and

we show that the tool often performs significantly better on standard

benchmarks than a tool based on a pure CEGIS approach.