Methods for program synthesis from formal specifications typically come in two flavors: top-down and bottom-up. Bottom-up program synthesis methods maintain a pool of complete programs and progressively generate new programs by composing existing ones. Top-down and bottom-up approaches have complementary strengths. For example, top-down methods work well when the specification can be naturally decomposed into subgoals through an analysis of partial programs. However, they can run into imprecision or computational complexity issues when the specification or the language semantics are complicated. In contrast, a bottom-up approach only needs to evaluate complete sub-expressions of a program, which is generally a much easier task than that of reasoning about partial programs.

Bottom-Up Synthesis with Recursion

Unfortunately, it is difficult to apply bottom-up synthesis to programming languages that permit recursion. This is because effective bottom-up approaches need to execute all sub-expressions of the target program; however, for recursive programs, sub-expressions can call the function being synthesized, whose semantics are still unknown. In this project, we introduce a new method for performing bottom-up synthesis in the presence of recursion. In this work, we apply a notion of angelic execution to synthesize recursive functions bottom-up.

This project is supported in part by NSF Award 1762299, NSF Award 1811865, NSF Award 191865, DARPA Contract FA8750-20-C-0208, and US Air Force and DARPA Contract FA8750-20-C-0002.