# Program Synthesis using Abstraction Refinement

arXiv: https://arxiv.org/abs/1710.07740 · HTML: https://mlsanity.com/paper/1710.07740/

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Oct 2017.

## Built on by (most cited first, 13 of 13)

- [Magicoder: Empowering Code Generation with OSS-Instruct](https://mlsanity.com/paper/2312.02120/) (2023)
- [API-guided Dataset Synthesis to Finetune Large Code Models](https://mlsanity.com/paper/2408.08343/) (2024)
- [Unsupervised Learning of Neurosymbolic Encoders](https://mlsanity.com/paper/2107.13132/) (2021)
- [Program Synthesis with Best-First Bottom-Up Search](https://mlsanity.com/paper/2310.04327/) (2023)
- [CodeEvo: Interaction-Driven Synthesis of Code-centric Data through Hybrid and Iterative Feedback](https://mlsanity.com/paper/2507.22080/) (2025)
- [Neural Architecture Search using Property Guided Synthesis](https://mlsanity.com/paper/2205.03960/) (2022)
- [Efficient Bottom-Up Synthesis for Programs with Local Variables](https://mlsanity.com/paper/2311.03705/) (2023)
- [Inductive Program Synthesis over Noisy Datasets using Abstraction Refinement Based Optimization](https://mlsanity.com/paper/2104.13315/) (2021)
- [Refinement Type Directed Search for Meta-Interpretive-Learning of Higher-Order Logic Programs](https://mlsanity.com/paper/2102.12553/) (2021)
- [Program Synthesis Over Noisy Data with Guarantees](https://mlsanity.com/paper/2103.05030/) (2021)
- [Abstract Interpretation for Generalized Heuristic Search in Model-Based Planning](https://mlsanity.com/paper/2208.02938/) (2022)
- [Towards Certificate-Driven Software Porting: A Self-Improving Agentic Harness for Scientific Program Optimization](https://mlsanity.com/paper/2609.34069/) (2026)
- [Assembling Insights for Agentic Machine Learning Engineering Systems](https://mlsanity.com/paper/2610.04927/) (2026)

## Abstract (arXiv)

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.