SHF: Medium: Compositional Semantics-Guided Synthesis

程序综合领域的目标是创建能够根据所需行为规范自动创建程序的工具。合成有望减轻程序员的负担(例如，通过自动找到棘手特殊情况的解决方案)，并允许非程序员仅通过指示他们希望程序产生的结果来创建程序。不幸的是，目前的合成工具无法解决大规模编程问题，这种情况可能会使这项前景光明的技术成为一个利基领域。该项目的新奇之处在于利用程序合成中的可组合性，使人们能够从较小的程序中创建更大的程序。该项目建立在最近名为SemGuS(语义引导合成)的框架之上，该框架为程序合成的可表现性和可伸缩性问题提供了一个立足点。原则上，该框架可以支持分层的软件综合，其中一个层中的实现选择对其他层隐藏(因此与信息隐藏的模块化软件设计一致)。该项目的目标是利用SemGuS提供的机会，将合成扩展到比迄今可能的更大的系统。这项工作将导致更可扩展和通用的合成算法，对已经广泛使用的合成应用具有潜在的好处。SemGuS框架的进一步发展有可能使合成更有用和更可编程，从而允许用户在不事先了解现有合成工具的情况下执行合成任务。最重要的是，成分合成将允许合成扩大到更大的应用，具有更实际的相关性。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

The field of program synthesis aims to create tools that can automatically create a program from a specification of desired behavior. Synthesis holds the promise of easing the burden on programmers (e.g., by finding solutions to tricky special cases automatically), and allowing non-programmers to create programs merely by indicating the outcome that they want the program to produce. Unfortunately, current synthesis tools do not scale up to large-scale programming problems, a situation that threatens to doom this promising technology to being a niche field. This project's novelties are ways to exploit compositionality in program synthesis in a way that allows one to create bigger programs out of smaller ones.The project builds on a recent framework called SemGuS (Semantics-Guided Synthesis), which offers a foothold on the expressibility and scalability problems of program synthesis. In principle, the framework can support the synthesis of software in layers, where implementation choices in one layer are hidden from other layers (and thus consistent with modular software design with information hiding). The goal of the project is to capitalize on the opportunity that SemGuS offers for extending synthesis to much larger systems than was possible heretofore. The work will lead to more scalable and general synthesis algorithms, with potential benefits to synthesis applications that are already in widespread use. Further development of the SemGuS framework has the potential to make synthesis more usable and programmable, and thereby allow users to carry out synthesis tasks without prior knowledge of existing synthesis tools. Most importantly, compositional synthesis will allow synthesis to scale to larger applications with more practical relevance.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.