The Sketching Approach to Program Synthesis

Tutorial at the 33rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI)

Date: Saturday June 16
Presenter: Armando Solar-Lezama
Duration: Half a day


The Sketch synthesis system allows programmers to write complex routines while leaving fragments of the code unspecified; the contents of these "holes" in the program is derived automatically by a synthesis engine. Sketching allows programmers to focus the power of the synthesizer on those portions of the code that are menial but easy to get wrong, reducing programmer effort without overwhelming the synthesizer.

This tutorial will offer a hands-on introduction to sketching as implemented in the SKETCH language and its accompanying synthesizer. The semantics of the different constructs in the language will be illustrated through simple examples and short programming exercises that participants will be able to try either by installing the tool or by using the web-version of the system. The tutorial will also show how the synthesizer can be used to derive the low-level details in a complex algorithm from a sketch that expresses its high-level structure. Basic sketching techniques will be illustrated through examples involving manipulations of linked data-structures, low-level bit-manipulation algorithms such as ciphers and error correction codes, and stencil kernels from scientific computing.

Target Audience
The target audience for the tutorial includes people who are interested in conducting program synthesis research, and who want to get hands-on experience with a state-of-the-art system. More broadly, the tutorial should be of interest to anyone with an interest in learning about a new and powerful programming technology.

Presenter Biography
Armando Solar-Lezama is an assistant professor in the electrical engineering and computer science department at MIT. His research interests lay in the area of computer supported programming; in particular, he is interested in program synthesis and program analysis tools to support programmer productivity. He earned his PhD in computer science at the University of California at Berkeley in 2008, where he originally developed the Sketching programming model together with his advisor Ras Bodik.

Additional information

You can play with the sketch language through the web version. The complete system is available in open source from bitbucket together with documentation. It is also recommended that you read the sketch language reference manual which describes the basic constructs of the language and includes several useful examples.

Easy to install distributions with pre-built JAR files

Source Precompiled for Windows (zip), or tar.gz Precompiled for Mac (Snow Leopard)

Exercise Source Files

karatsuba, list reversal