Dana Drachsler Cohen

Date: 17:00, Wednesday, November 22, 2017
Speaker: Dana Drachsler Cohen
Venue: IST Austria

Mondi 2

Interactive program synthesizers enable a user to communicate his/her intent via input-output examples. Unfortunately, such synthesizers only guarantee that the synthesized program is correct on the provided examples. A user that wishes to guarantee correctness for all possible inputs has to manually inspect the synthesized program, an error-prone and challenging task.
In this talk, I will present a novel synthesis framework that communicates only through (abstract) examples and guarantees that the synthesized program is correct on all inputs.
The main idea is to use abstract examples—a new form of examples that represent a potentially unbounded set of concrete examples. An abstract example captures how part of the input space is mapped to corresponding outputs by the synthesized program. Our framework uses a generalization algorithm to compute abstract examples which are then presented to the user. The user can accept an abstract example, or provide a counterexample in which case the synthesizer will explore a different program. When the user accepts a set of abstract examples that covers the entire input space, the synthesis process is completed.
I will also show some experimental results to demonstrate that our synthesizer communicates with the user effectively.
Joint work with Sharon Shoham and Eran Yahav.
Posted in RiSE Seminar