http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FM7BodikWG211/M7Bodik - Revision history2026-04-05T22:43:50ZRevision history for this page on the wikiMediaWiki 1.43.5http://mw.hh.se/wg211/index.php?title=WG211/M7Bodik&diff=221&oldid=prevAdmin: 1 revision2011-12-12T10:06:27Z<p>1 revision</p>
<p><b>New page</b></p><div>[[Category:WG211]]<br />
<br />
<br />
<h1>Program Synthesis by Sketching</h1><br />
<h3>Rastislav Bodik</h3><br />
<br />
Software synthesis automatically derives programs that are efficient,<br />
even surprising, but it requires a domain theory, elusive for many<br />
applications. Trying to make synthesis accessible, we style the<br />
synthesizer into a programmer assistant: the programmer writes a partial<br />
program that elides tricky code fragments and the synthesizer completes<br />
the program to match a specification. Our hypothesis is that the partial<br />
program, called a sketch, communicates the programmer insight to the<br />
synthesizer more naturally than a domain theory.<br />
<br />
On the algorithmic side, sketching exploits recent advances in automated<br />
decision procedures. This talk will show how we turned a program checker<br />
into a synthesizer with a counterexample-guided inductive synthesis. I<br />
will also describe the SKETCH language and its linguistic support for<br />
synthesis and show how we synthesized complex implementations of<br />
ciphers, scientific codes, and even concurrent lock-free<br />
data-structures.<br />
<br />
Joint work with Armando Solar-Lezama, Chris Jones, Gilad Arnold, Lexin<br />
Shan, Satish Chandra and many others.<br />
<br />
* [[Media:bodik-wg09.ppt | bodik-wg09.ppt ]]: Slides<br />
<br />
==File Attachments== <br />
<br />
*[[Media:bodik-wg09.ppt | bodik-wg09.ppt]]</div>Admin