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 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
14:20 - 16:00
|Learning Programs from Noisy Data|
Veselin Raychev ETH Zurich, Pavol Bielik ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Andreas Krause ETH ZurichLink to publication DOI Pre-print Media Attached File Attached
|Optimizing Synthesis with Metasketches|
James Bornholt University of Washington, Emina Torlak University of Washington, Dan Grossman University of Washington, USA, Luis Ceze University of Washington, USAPre-print Media Attached
|Maximal Specification Synthesis|
Aws Albarghouthi University of Wisconsin–Madison, Isil Dillig University of Texas, Austin, Arie Gurfinkel Carnegie Mellon UniversityPre-print Media Attached
|Example-Directed Synthesis: A Type-Theoretic Interpretation|
Jonathan Frankle Princeton University, Peter-Michael Osera Grinnell College, David Walker Princeton University, Steve Zdancewic University of PennsylvaniaPre-print Media Attached File Attached