Programmers would love to have their code synthesized but current synthesizers are narrowly domain-specific and require expert guidance. Sketching attempts to bring software synthesis to everyday programming by making synthesizer a programmer assistant. In this approach, the programmer writes a sketch---a program that leaves out tricky code fragments such as array index expressions. The synthesizer completes the sketch to make it behave like a separately provided behavioral specification. Buggy sketches are rejected, yielding correctness by construction.
I will describe the SKETCH language and its linguistic support for sketch-based synthesis. I will then focus on the SKETCH combinatorial (2QBF) synthesizer, which finds the program by a counterexample-driven search. The synthesizer obtains programs that are guaranteed correct in a bounded input space; I will show how to synthesize some classes of unbounded programs. I will conclude by reporting our results with sketching of real-world cryptographic codes and structured grid methods.