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
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

10:30 - 11:35: Research Papers - Synthesis at Ile de France III (IDF III)
Chair(s): Mohsen LesaniUniversity of California, Riverside
POPL-2020-Research-Papers10:30 - 10:51
Suguman BansalRice University, USA, Kedar NamjoshiBell Labs, Nokia, Yaniv Sa'arNokia Bell Labs, Kfar Saba, Israel
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers10:51 - 11:13
Shengwei AnPurdue University, Rishabh SinghGoogle Brain, Sasa MisailovicUniversity of Illinois at Urbana-Champaign, Roopsha SamantaPurdue University
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers11:13 - 11:35
Mukund RaghothamanUniversity of Southern California, Jonathan MendelsonUniversity of Pennsylvania, David ZhaoThe University of Sydney, Mayur NaikUniversity of Pennsylvania, Bernhard ScholzUniversity of Sydney, Australia
Link to publication DOI Media Attached File Attached