Thu 21 Jun 2018 14:25 - 14:50 at Grand Ballroom CD - Synthesis and Learning Chair(s): Xin Zhang

We propose a new conflict-driven program synthesis technique that is capable of learning from past mistakes. Given a spurious program that violates the desired specification, our synthesis algorithm identifies the root cause of the conflict and learns new lemmas that can prevent similar mistakes in the future. Specifically, we introduce the notion of equivalence modulo conflict and show how this idea can be used to learn useful lemmas that allow the synthesizer to prune large parts of the search space. We have implemented a general-purpose CDCL-style program synthesizer called Neo and evaluate it in two different application domains, namely data wrangling in R and functional programming over lists. Our experiments demonstrate the substantial benefits of conflict-driven learning and show that Neo outperforms two state-of-the-art synthesis tools, Morpheus and Deepcoder, that target these respective domains.

Conference Day
Thu 21 Jun

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:40
Synthesis and LearningPLDI Research Papers at Grand Ballroom CD
Chair(s): Xin ZhangMassachusetts Institute of Technology, USA
14:00
25m
Talk
A General Path-Based Representation for Predicting Program Properties
PLDI Research Papers
Uri AlonTechnion, Meital ZilbersteinTechnion, Omer LevyUniversity of Washington, USA, Eran YahavTechnion
Media Attached
14:25
25m
Talk
Program Synthesis using Conflict-Driven Learning
PLDI Research Papers
Yu FengUniversity of Texas at Austin, USA, Ruben MartinsCarnegie Mellon University, Osbert BastaniStanford University, Isil DilligUT Austin
Media Attached
14:50
25m
Talk
Accelerating Search-Based Program Synthesis using Learned Probabilistic Models
PLDI Research Papers
Woosuk LeeUniversity of Pennsylvania, USA, Kihong HeoUniversity of Pennsylvania, USA, Rajeev AlurUniversity of Pennsylvania, Mayur NaikUniversity of Pennsylvania
Media Attached
15:15
25m
Talk
Inferring Crypto API Rules from Code Changes
PLDI Research Papers
Media Attached