Abstract
Constraint-based program synthesis techniques have been widely used in numerous settings. However, synthesizing programs that use libraries remains a major challenge. To handle complex or black-box libraries, the state of the art is to provide carefully crafted mocks or models to the synthesizer, requiring extra manual work. We address this challenge by proposing Toshokan, a new synthesis framework as an alternative approach in which library-using programs can be generated without any user-provided artifacts at the cost of moderate performance overhead. The framework extends the classic counterexample-guided synthesis framework with a bootstrapping, log-based library model. The model collects input-output samples from running failed candidate programs on witness inputs. We prove that the framework is sound when a sound, bounded verifier is available, and also complete if the underlying synthesizer and verifier promise to produce minimal outputs. We implement and incorporate the framework to JSketch, a Java sketching tool. Experiments show that Toshokan can successfully synthesize programs that use a variety of libraries, ranging from mathematical functions to data structures.
Biography
I am a Ph.D. candidate at ECE Purdue University working with Prof. Xiaokang Qiu. I am broadly interested in Program Synthesis, Formal Methods, Compilers and Programming Languages at large. My thesis research focuses on modular techniques for program synthesis with libraries, and the topic of this talk is a major part of my thesis research.