Synthesizing Programs from Programmer Insight

   Ras Bodik, UC Berkeley
    bodikcs.berkeley.edu

Seminar on People, Computers, and Design
Stanford University October 9, 2009, 12:50-2:05pm, Gates B01

Massive compute power has long been available to us but we need more ideas on how to harness it in programming. While testing and verification dutifully number-crunch programs, they do not fix the bugs they find. Moving closer to programmers, recent tools have become true cognitive assistants: search engines find relevant code samples, verifiers explain bugs, and software miners discover properties absent in the documentation. Still, these tools do not directly address the problem of writing programs.

This talk will describe a growing family of programmer tools that assist in writing programs. Their premise is that programs can be decomposed into insight and mechanics, and that the later can be synthesized from the former. The first research problem is how to describe the insight without spelling out the details. I will describe the idea of sketching (programs with holes) and how we move beyond programming by demonstration by asking an oracle for a demonstration. The second problem is how to synthesize the program from the insight. Some of our tools combine mining of examples with program analysis, and some rely on recent advances in decision procedures, such as SAT, that combine search with algebraic reasoning. I will conclude with open problems motivated by some of our more ambitious ideas.

Ras Bodik is Associate Professor of Computer Science at UC Berkeley. He is interested in programming systems, from the HCI aspect of programmer tool and language design, to program analysis, compilation, and computer architecture. He has worked on mining of program specifications, debugging. He is currently leading projects on synthesis for programmer masses and on a web browser for mobile devices.

The talks are open to the public. They are in the Gates Building, Room B01 in the basement. The nearest public parking is in the structure at Campus Drive and Roth Way.

View this talk on line at CS547 on Stanford OnLine or using this video link.

Titles and abstracts for previous years are available by year and by speaker.