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

SHF：小型：使用反例引导的抽象细化的可扩展程序综合

• 批准号: 1811865
• 负责人: Isil Dillig
• 金额: $ 35万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-10-01 至 2023-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1811865&HistoricalAwards=false
• 关键词: SHF; Small; Scalable; Program; Synthesis

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.

程序合成的领域有望通过自动从高级规格（例如输入输出示例）生成程序来大大简化软件开发。尽管有关程序合成的最新研究已经进行了一系列，但就基本编程语言的复杂性以及可以合成的程序的复杂性而言，现有技术的可扩展性有限。该项目的主要目的是通过开发更有效，更可扩展的合成技术来推进程序合成的最先进。这项研究可能会扩大程序综合的适用性和可扩展性，这可以使最终用户和程序员都具有破坏性更改。调查人员将在该项目中包括研究生和本科生。该项目使用抽象细化（同步）​​范式研究了合成的基础和实例。在同步范式中，一个抽象合成器生成的候选程序可以满足相对于抽象语义的规范，而抽象完善引擎构建了新的抽象，这些抽象排除了抽象合成器返回的虚假程序。在研究人员先前完成的工作的基础上，该项目开发了（a）新的抽象合成算法，这些算法可以有效地处理更丰富的语言特征，例如递归和高阶功能； （b）自动化和有效的抽象细化算法； （c）可以从以前的迭代中重用知识的增量合成技术； （d）规范推理技术，以减少整合合成器可以使用的新原语所需的精力。 该项目将开发工具并将这些想法应用于不同领域，例如数值/统计计算，文本处理以及使用复杂的应用程序程序员界面（API）进行编程。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子优点和更广泛的审查标准来通过评估来通过评估来支持的。