Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Fri 25 Oct 2019 14:22 - 14:45 at Attica - Synthesis Chair(s): Christoph Reichenbach

A key challenge in program synthesis is synthesizing programs that use libraries, which most real-world software does. The current state of the art is to model libraries with mock library implementations that perform the same function in a simpler way. However, mocks may still be large and complex, and must include many implementation details, both of which could limit synthesis performance. To address this problem, we introduce JLibSketch, a Java program synthesis tool that allows library behavior to be described with algebraic specifications, which are rewrite rules for sequences of method calls, e.g., encryption followed by decryption (with the same key) is the identity. JLibSketch implements rewrite rules by compiling JLibSketch problems into problems for the Sketch program synthesis tool. More specifically, after compilation, library calls are represented by abstract data types (ADTs), and rewrite rules manipulate those ADTs. We formalize compilation and prove it sound and complete if the rewrite rules are ordered and non-unifiable. We evaluated JLibSketch by using it to synthesize nine programs that use libraries from three domains: data structures, cryptography, and file systems. We found that algebraic specifications are, on average, about half the size of mocks. We also found that algebraic specifications perform better than mocks on seven of the nine programs, sometimes significantly so, and perform equally well on the last two programs. Thus, we believe that JLibSketch takes an important step toward synthesis of programs that use libraries.

Fri 25 Oct

Displayed time zone: Beirut change

14:00 - 15:30
Synthesis OOPSLA at Attica
Chair(s): Christoph Reichenbach Lund University
14:00
22m
Talk
AL: Autogenerating Supervised Learning Programs
OOPSLA
DOI
14:22
22m
Talk
Program Synthesis with Algebraic Library Specifications
OOPSLA
Benjamin Mariano University of Maryland, College Park, Josh Reese University of Maryland, College Park, Siyuan Xu Purdue University, ThanhVu Nguyen University of Nebraska, Lincoln, Xiaokang Qiu Purdue University, Jeffrey S. Foster Tufts University, Armando Solar-Lezama Massachusetts Institute of Technology
DOI
14:45
22m
Talk
AutoPandas: Neural-Backed Generators for Program Synthesis
OOPSLA
Rohan Bavishi UC Berkeley, Caroline Lemieux University of California, Berkeley, Roy Fox UC Berkeley, Koushik Sen University of California, Berkeley, Ion Stoica UC Berkeley
DOI
15:07
22m
Talk
On the Fly Synthesis of Edit Suggestions
OOPSLA
Anders Miltner Princeton University, Sumit Gulwani Microsoft, Vu Le Microsoft, Alan Leung Microsoft, Arjun Radhakrishna Microsoft, Gustavo Soares Microsoft, Ashish Tiwari Microsoft, Abhishek Udupa Microsoft
DOI Pre-print Media Attached