SHF: Medium: Compositional Semantics-Guided Synthesis

University Of Wisconsin-Madison, Madison WI

Investigators

Abstract

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.