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

程序综合领域承诺通过从高级规范(例如输入-输出示例)自动生成程序来极大地简化软件开发。虽然最近有一系列关于程序综合的研究，但现有技术在底层编程语言的复杂性以及可以综合的程序的复杂性方面都具有有限的可扩展性。该项目的主要目标是通过开发更高效和可伸缩的合成技术来提高程序合成的最新水平。这项研究可能会扩大程序合成的适用性和可扩展性，这可能会对最终用户和程序员都产生破坏性的变化。调查员将包括研究生和本科生参加这个项目。这个项目研究了使用抽象精化(SYNGAR)范式进行综合的基础和实例。在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.