Rastislav Bodik
Computer Science
Division
University of California, Berkeley
"Algorithmic Program Synthesis with Partial Programs"
Abstract
Why hasn’t Moore’s Law revolutionize programming? In model checking, cycles fuel bug discovery, improving code quality, but programmers still write programs with their bare hands. In fact, their work has not changed much since the CRT terminal, except that they think in better languages.
Program synthesis might be a way to reduce the programmer’s cognitive load. Synthesizers have derived programs that were highly efficient, and sometimes even surprising. Of course, they had to be first "programmed" with the human insights about the domain at hand.
Which brings us to a key problem in program synthesis --- how to communicate human expertise to the synthesizer. In deductive synthesis, this expertise is captured in a domain theory. Often elusive even to formally trained experts, a domain theory is probably not a shortcut to programmer productivity.
This talk will describe a growing family of synthesizers based on partial programs. Their premise is that programs can be decomposed into insight and mechanics: if the programmer encodes her insight as a partial program, the mechanics can then be synthesized given a specification. Partial programs lend themselves to algorithmic synthesis: rather than deducing a program with a theorem prover, algorithmic synthesis finds the program in a space of candidate implementations described by the partial program.
Among five synthesizers, I will describe an algorithm for finding a candidate by constraint solving, rather than via generate-and-test, and a system for programming with angelic non-determinism which computes the insight into a programming problem.
Bio:
Ras Bodik is an Associate Professor of Computer Science at UC Berkeley. He is interested in programming systems, from static and dynamic analysis to programmer tools. He leads a project of program synthesis for high-performance programs based on the idea of program sketches. He also leads a project on parallel web browsers for mobile devices, which develops parallel parsing and page layout algorithms, as well as a constraints-based scripting language.
Tuesday, October 20, 2009
3:00 - 4:15
Wu & Chen
101 Levine Hall