Program synthesis using abstraction refinement
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Dec 27, 2017
- Source ID
- 10.1145/3158151
Entities
People
- Işıl Dillig
- Rishabh Singh
- Xinyu Wang
Organizations
- Air Force Research Laboratory
- Microsoft
- National Science Foundation
- University of Texas at Austin