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

程序综合领域通过从高级规范（如输入输出示例）自动生成程序，有望极大地简化软件开发。虽然最近有一系列关于程序合成的研究，但现有技术在底层编程语言的复杂性以及可以合成的程序的复杂性方面都具有有限的可扩展性。这个项目的主要目标是通过开发更有效和可扩展的合成技术来推进程序合成的最新发展。这项研究可能会扩大程序合成的适用性和可扩展性，这可能会使最终用户和程序员的破坏性变化。研究者将包括研究生和本科生在这个项目。本计画探讨抽象化合成的基础与实例化。在SYNGAR范例中，抽象合成器生成满足关于抽象语义的规范的候选程序，并且抽象细化引擎构造排除由抽象合成器返回的伪程序的新抽象。在研究人员以前所做工作的基础上，该项目开发（a）新的抽象综合算法，可以有效地处理更丰富的语言特征，如递归和高阶函数;（B）自动化的&高效抽象细化算法;（c）增量综合技术，可以重用以前迭代的知识;以及（d）规范推断技术，以减少集成可由合成器使用的新原语所需的努力。 该项目将开发工具，并将这些想法应用于不同的领域，如数值/统计计算，文本处理和复杂的应用程序接口（API）编程。该奖项反映了NSF的法定使命，并已被认为是值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估的支持。

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.