Program Synthesis by Sketching

Date: 
Thursday, February 28, 2008 - 5:01pm


UCSB COMPUTER SCIENCE DEPARTMENT PRESENTS FACULTY CANDIDATE:
ARMANDO SOLAR-LEZAMA Department of Computer Science University of California, Berkeley

DATE: MONDAY, MARCH 10, 2008
TIME: 3:30 – 4:30 p.m.
PLACE: Computer Science Conference Room, Harold Frank Hall Rm. 1132

ABSTRACT:
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. The potential for synergy exists because the synthesizer needs human insight to discover acceptable implementations from the universe of unacceptable ones. At the same time, programmers actually want control over the implementation strategy. Thus, practical synthesis must allow programmers to guide the synthesis process, but in a natural way, without having to axiomatize their insights into domain theories, as many traditional synthesis tools require.

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.

BIOGRAPHY:
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.

HOST: CHANDRA KRINTZ