- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- BIRS Workshop Lecture Videos /
- Conflict-Driven Synthesis
Open Collections
BIRS Workshop Lecture Videos
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 Metadata
Title |
Conflict-Driven Synthesis
|
Creator | |
Publisher |
Banff International Research Station for Mathematical Innovation and Discovery
|
Date Issued |
2018-08-30T13:15
|
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. |
Extent |
33.0
|
Subject | |
Type | |
File Format |
video/mp4
|
Language |
eng
|
Notes |
Author affiliation: Carnegie Mellon University
|
Series | |
Date Available |
2019-04-05
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
Attribution-NonCommercial-NoDerivatives 4.0 International
|
DOI |
10.14288/1.0377823
|
URI | |
Affiliation | |
Peer Review Status |
Unreviewed
|
Scholarly Level |
Other
|
Rights URI | |
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
Attribution-NonCommercial-NoDerivatives 4.0 International