Write a Blog >>
Thu 23 Jan 2020 11:13 - 11:35 at Ile de France III (IDF III) - Synthesis Chair(s): Mohsen Lesani

We propose a new approach to synthesize Datalog programs from input-output specifications. Our approach leverages query provenance to scale the counterexample-guided inductive synthesis (CEGIS) procedure for program synthesis. In each iteration of the procedure, a SAT solver proposes a candidate Datalog program, and a Datalog solver evaluates the proposed program to determine whether it meets the desired specification. Failure to satisfy the specification results in additional constraints to the SAT solver. We propose efficient algorithms to learn these constraints based on “why” and “why not” provenance information obtained from the Datalog solver. We have implemented our approach in a tool called ProSynth and present experimental results that demonstrate significant improvements over the state-of-the-art, including in synthesizing invented predicates, reducing running times, and in decreasing variances in synthesis performance. On a suite of 40 synthesis tasks from three different domains, ProSynth is able to synthesize the desired program in 10 seconds on average per task—an order of magnitude faster than baseline approaches—and takes only under a second each for 28 of them.

Slides (main.pptx)3.31MiB

Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 11:35
SynthesisResearch Papers at Ile de France III (IDF III)
Chair(s): Mohsen Lesani University of California, Riverside
10:30
21m
Talk
Synthesis of Coordination Programs from Linear Temporal Specifications
Research Papers
Suguman Bansal Rice University, USA, Kedar Namjoshi Bell Labs, Nokia, Yaniv Sa'ar Nokia Bell Labs, Kfar Saba, Israel
Link to publication DOI Media Attached File Attached
10:51
21m
Talk
Augmented Example-based Synthesis using Relational Perturbation Properties
Research Papers
Shengwei An Purdue University, Rishabh Singh Google Brain, Sasa Misailovic University of Illinois at Urbana-Champaign, Roopsha Samanta Purdue University
Link to publication DOI Media Attached File Attached
11:13
21m
Talk
Provenance-Guided Synthesis of Datalog Programs
Research Papers
Mukund Raghothaman University of Southern California, Jonathan Mendelson University of Pennsylvania, David Zhao The University of Sydney, Mayur Naik University of Pennsylvania, Bernhard Scholz University of Sydney, Australia
Link to publication DOI Media Attached File Attached