WG211/M7Bodik
Program Synthesis by Sketching
Rastislav Bodik
Software synthesis automatically derives programs that are efficient, even surprising, but it requires a domain theory, elusive for many applications. Trying to make synthesis accessible, we style the synthesizer into a programmer assistant: the programmer writes a partial program that elides tricky code fragments and the synthesizer completes the program to match a specification. Our hypothesis is that the partial program, called a sketch, communicates the programmer insight to the synthesizer more naturally than a domain theory.
On the algorithmic side, sketching exploits recent advances in automated decision procedures. This talk will show how we turned a program checker into a synthesizer with a counterexample-guided inductive synthesis. I will also describe the SKETCH language and its linguistic support for synthesis and show how we synthesized complex implementations of ciphers, scientific codes, and even concurrent lock-free data-structures.
Joint work with Armando Solar-Lezama, Chris Jones, Gilad Arnold, Lexin Shan, Satish Chandra and many others.
- bodik-wg09.ppt : Slides
