Write a Blog >>
Fri 22 Jan 2016 14:45 - 15:10 at Grand Bay North - Track 1: Synthesis Chair(s): Roberto Giacobazzi

Many advanced programming tools—for both end-users and expert developers—rely on program synthesis to automatically generate implementations from high-level specifications. These tools often need to employ tricky, custom-built synthesis algorithms because they require synthesized programs to be not only correct, but also optimal with respect to a desired cost metric, such as program size. Finding these optimal solutions efficiently requires domain-specific search strategies, but existing synthesizers hard-code the strategy, making them difficult to reuse.

This paper presents metasketches, a general framework for specifying and solving optimal synthesis problems. Metasketches make the search strategy a part of the problem definition by specifying a fragmentation of the search space into an ordered set of classic sketches. We provide two cooperating search algorithms to effectively solve metasketches. A global optimizing search coordinates the activities of local searches, informing them of the costs of potentially-optimal solutions as they explore different regions of the candidate space in parallel. The local searches execute an incremental form of counterexample-guided inductive synthesis to incorporate information sent from the global search. We present Synapse, an implementation of these algorithms, and show that it effectively solves optimal synthesis problems with a variety of different cost functions. In addition, metasketches can be used to accelerate classic (non-optimal) synthesis by explicitly controlling the search strategy, and we show that Synapse solves classic synthesis problems that state-of-the-art tools cannot.

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 16:00
Track 1: SynthesisResearch Papers at Grand Bay North
Chair(s): Roberto GiacobazziUniversity of Verona, Italy
14:20
25m
Talk
Learning Programs from Noisy Data
Research Papers
Veselin RaychevETH Zurich, Pavol BielikETH Zurich, Switzerland, Martin VechevETH Zurich, Andreas KrauseETH Zurich
Link to publication DOI Pre-print Media Attached File Attached
14:45
25m
Talk
Optimizing Synthesis with Metasketches
Research Papers
James BornholtUniversity of Washington, Emina TorlakUniversity of Washington, Dan GrossmanUniversity of Washington, USA, Luis CezeUniversity of Washington, USA
Pre-print Media Attached
15:10
25m
Talk
Maximal Specification Synthesis
Research Papers
Aws AlbarghouthiUniversity of Wisconsin–Madison, Isil DilligUniversity of Texas, Austin, Arie GurfinkelCarnegie Mellon University
Pre-print Media Attached
15:35
25m
Talk
Example-Directed Synthesis: A Type-Theoretic Interpretation
Research Papers
Jonathan FranklePrinceton University, Peter-Michael OseraGrinnell College, David WalkerPrinceton University, Steve ZdancewicUniversity of Pennsylvania
Pre-print Media Attached File Attached