Sketch Internals Tutorial

The Sketch synthesis system is an open source infrastructure for program synthesis that has been used in a variety of research projects in academia and industrial research labs. Sketch is based on a powerful symbolic search procedure that allows users to describe spaces of possible programs and then automatically search that space for a program that satisfies a given specification.
In this hands-on tutorial, I will cover the internals of the Sketch synthesis system and some of the key algorithms behind it. The tutorial is aimed at students and researchers who wish to contribute to the Sketch synthesizer or simply gain a better understanding of how the system works in order to use it more effectively.