Fri 9 Nov 2018 10:30 - 10:52 at Studio 2 - Program Synthesis Chair(s): Jens Palsberg

This paper proposes relational program synthesis, a new problem that concerns synthesizing one or more programs that collectively satisfy a relational specification. As a dual of relational program verification, relational program synthesis is an important problem that has many practical applications, such as automated program inversion and automatic generation of comparators. However, this relational synthesis problem introduces new challenges over its non-relational counterpart due to the combinatorially larger search space. As a first step towards solving this problem, this paper presents a synthesis technique that combines the counterexample-guided inductive synthesis framework with a novel inductive synthesis algorithm that is based on relational version space learning. We have implemented the proposed technique in a framework called Relish, which can be instantiated to different application domains by providing a suitable domain-specific language and the relevant relational specification. We have used the Relish framework to build relational synthesizers to automatically generate string encoders/decoders as well as comparators, and we evaluate our tool on several benchmarks taken from prior work and online forums. Our experimental results show that the proposed technique can solve almost all of these benchmarks and that it significantly outperforms EUSolver, a generic synthesis framework that won the general track of the most recent SyGuS competition.

Fri 9 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:00
Program SynthesisOOPSLA at Studio 2
Chair(s): Jens Palsberg University of California, Los Angeles
10:30
22m
Talk
Relational Program Synthesis
OOPSLA
Yuepeng Wang University of Texas at Austin, Xinyu Wang UT Austin, Isil Dillig UT Austin
10:52
22m
Talk
Robust Relational Layout Synthesis from Examples for Android
OOPSLA
Pavol Bielik ETH Zürich, Marc Fischer ETH Zurich, Martin Vechev ETH Zürich
11:15
22m
Talk
Speeding up Symbolic Reasoning for Relational Queries
OOPSLA
Chenglong Wang University of Washington, USA, Alvin Cheung University of Washington, Rastislav Bodik University of Washington
11:37
22m
Talk
Automatic Diagnosis and Correction of Logical Errors for Functional Programming Assignments
OOPSLA
Junho Lee Korea University, Dowon Song Korea University, Sunbeom So Korea University, Hakjoo Oh Korea University