Sciweavers

OOPSLA
2015
Springer

Toward tool support for interactive synthesis

7 years 11 months ago
Toward tool support for interactive synthesis
Syntax-guided synthesis searches for an implementation of a given specification by exploring large spaces of candidate programs. Sketches reduce these search spaces, making synthesis more tractable, by predefining the structure of the desired implementation. Typically, this structure is obtained through human insight—this paper introduces a method for interactive, tool-supported discovery of such structure. The key idea is to decompose the specification into subcomputations such that the decomposition dictates the sketch. We rely on a readily obtainable specification that is nothing more than a finite set of sample input-output pairs or execution traces of the desired program. We introduce two complementary decomposition operators and demonstrate them on case studies. We find that our interactive methodology to discover structure extends the reach of computer-aided programming to problems that cannot be solved with synthesis alone. Categories and Subject Descriptors F.3.1 [Spe...
Shaon Barman, Rastislav Bodík, Satish Chand
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where OOPSLA
Authors Shaon Barman, Rastislav Bodík, Satish Chandra, Emina Torlak, Arka Bhattacharya, David Culler
Comments (0)