Program Synthesis by Sketching
Speaker: Armando Solar-Lezama , University of California at Berkeley
Date: March 17 2008
Time: 4:00PM to 5:00PM
Location: 32-G449, Patil/Kiva
Host: John Guttag, MIT
Contact: Francis Doughty, 253-4602, doughty@mit.edu
Relevant URL: For over thirty years, software synthesis has promised to automate the chore of writing programs. But only recently, the power of modern computers and the growing maturity of verification technology have combined to make practical synthesis possible.
One of the biggest challenges for practical synthesis is to establish a synergy between the synthesizer and the programmer. There is potential for synergy because, while the synthesizer needs human insight to produce acceptable implementations, programmers actually want control over the implementation strategy, so they want to be able to guide the synthesis process. Thus, both the programmer and the synthesizer benefit when programmers are allowed to provide insight in a natural way.
Sketching is my answer to the challenges of practical synthesis. It is a form of synthesis whose key novelty is the use of partial programs (sketches) to communicate insight to the synthesizer.
The talk will describe sketching as implemented in the SKETCH language, and the innovations in inductive synthesis that made sketching possible. The talk will also describe our experience using SKETCH to synthesize complex implementations of ciphers, scientific codes, and even concurrent lock-free data-structures.
Bio:
Armando Solar-Lezama is a student of Rastislav Bodik at UC Berkeley working on software synthesis. His main interests include programming languages, compilers and parallel computing. Before coming to Berkeley, he completed BS degrees in Math and CS at Texas A&M University, where he also worked as a programmer writing massively parallel neutron transport simulations. His broad agenda is to exploit the growing availability of computing power and formal methods to make programming easier.
See other events that are part of CS Special Seminar Series Spring 2008
See other events happening in March 2008
