  We present a new approach to example-guided program synthesis based on
counterexample-guided abstraction refinement. Our method uses the abstract
semantics of the underlying DSL to find a program $P$ whose abstract behavior
satisfies the examples. However, since program $P$ may be spurious with respect
to the concrete semantics, our approach iteratively refines the abstraction
until we either find a program that satisfies the examples or prove that no
such DSL program exists. Because many programs have the same input-output
behavior in terms of their abstract semantics, this synthesis methodology
significantly reduces the search space compared to existing techniques that use
purely concrete semantics. While synthesis using abstraction refinement
(SYNGAR) could be implemented in different settings, we propose a
refinement-based synthesis algorithm that uses abstract finite tree automata
(AFTA). Our technique uses a coarse initial program abstraction to construct an
initial AFTA, which is iteratively refined by constructing a proof of
incorrectness of any spurious program. In addition to ruling out the spurious
program accepted by the previous AFTA, proofs of incorrectness are also useful
for ruling out many other spurious programs. We implement these ideas in a
framework called \tool. We have used the BLAZE framework to build synthesizers
for string and matrix transformations, and we compare BLAZE with existing
techniques. Our results for the string domain show that BLAZE compares
favorably with FlashFill, a domain-specific synthesizer that is now deployed in
Microsoft PowerShell. In the context of matrix manipulations, we compare BLAZE
against Prose, a state-of-the-art general-purpose VSA-based synthesizer, and
show that BLAZE results in a 90x speed-up over Prose.
