BIRS Workshop Lecture Videos

Banff International Research Station Logo

BIRS Workshop Lecture Videos

Conflict-Driven Synthesis Martins, Ruben

Description

Program synthesis is expanding rapidly and getting a lot of attention from both industry and academia. The goal of program synthesis is to find a program that satisfies the user intent expressed in the form of some specification. Program synthesis has proven to be useful to both end-users and programmers. For instance, program synthesis has been used to automate tedious tasks that arise in everyday life, such as string manipulations in spreadsheets or data wrangling tasks in R. Program synthesis has also been used for improving programmer productivity by automatically completing parts of a program or helping programmers use complex APIs.

In this talk, I will present a new conflict-driven program synthesis framework that is capable of learning from past mistakes. Given a 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. 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 an order of magnitude improvement when using conflict-driven learning and opens a new research direction that can push the boundaries of program synthesis.

Item Media

Item Citations and Data

Rights

Attribution-NonCommercial-NoDerivatives 4.0 International