SKETCH is a sketching system based on combinatorial search, as opposed to transformations. In this system, the sketch is given in the form of a partial program--a program with holes--and the sketch resolution synthesizes code to fill in the holes. The holes may stand for index expressions, lookup tables or bitmasks, and the programmer can easily define new kinds of holes with the synthesis operators provided. SKETCH completes sketches by means of a combinatorial search based on generalized boolean satisfiability.

The some of the  main contributions of this project include:

• Design of a language for sketching based on a single new construct: the integer hole which the synthesizer replaces with an integer constant. This construct is incredibly powerful; by composing expressions with integer holes and composing them into libraries, we can provide the programmer with a rich language for expressing intent while leaving low-level details unspecified.
• Reduction of the synthesis problem to a generalized boolean satisfiability problem. Because all the holes in the sketch are expressed in terms of integer holes, the synthesis problem can be framed as a search for a set of integer constants that make the spec equal the sketch for all inputs. 
• A counterexample guided algorithm to solve sketch synthesis problems.
• Development of a robust implementation of the sketch language available for download here.
  

The basic combinatorial sketch solver has been released, and can be found here, together with a useful tutorial. The compiler release currently includes only the functionality up to the ASPLOS 06 paper. By Jan 08, we intend to release version 1.2, which will include the code for synthesizing stencils, as described in PLDI 07, as well as support for pointers and heap-based data-structures, and improved error-messages and debugging output.

We are currently extending the synthesizer to be able to sketch concurrent and lock-free datastructures (more on this soon).

This is joint work Gilad Arnold, Chris Jones, Liviu Tacanu, and my advisor, Ras Bodik, in collaboration with Sanjit Seshia, and Vijay Saraswat. We are also colaborating with Alan Mischenko and Satrajit Chatterjee, from Robert Brayton's group, to incorporate some of their verification technology into our solver.