SHF: Small: Scalable Program Synthesis using Counterexample-Guided Abstraction Refinement

University Of Texas At Austin, Austin TX

Investigators

Abstract

The field of program synthesis promises to dramatically simplify software development by automatically generating programs from high-level specifications, such as input-output examples. While there has been a flurry of recent research on program synthesis, existing techniques have limited scalability both in terms of the complexity of the underlying programming language as well as the complexity of the programs that can be synthesized. The main goal of this project is to advance the state-of-the-art in program synthesis by developing much more efficient and scalable synthesis techniques. This research could potentially broaden the applicability and scalability of program synthesis which could enable disruptive changes to both end-users and programmers. The investigator will include both graduate and undergraduate students in this project. This project investigates the foundations and instantiations of the synthesis using abstraction refinement (SYNGAR) paradigm. In the SYNGAR paradigm, an abstract synthesizer generates candidates programs that satisfy the specification with respect to an abstract semantics, and an abstraction refinement engine constructs new abstractions that rule out spurious programs returned by the abstract synthesizer. Building on previous work done by the investigators, the project develops (a) new abstract synthesis algorithms that can efficiently handle richer language features such as recursion and higher-order functions; (b) automated & efficient abstraction refinement algorithms; (c) incremental synthesis techniques that can reuse knowledge from previous iterations; and (d) specification inference techniques to reduce the effort required to integrate new primitives that can be used by the synthesizer. The project will develop tools and apply these ideas to different domains, such as numerical/statistical computing, text processing, and programming with complex Application Programmer Interfaces (APIs). This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.