Thursday, October 4, 2007
4:15 pm
B17 Upson Hall

Computer Science
Fall 2007

Rastislav Bodik
UC Berkeley

Programming by Sketching

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.