Recent years have witnessed resurgence of interest in software synthesis, spurred by growing software complexity and enabled by advances in verification and decision procedures. This seminar brought together veterans of deductive synthesis as well as representatives of new synthesis efforts. Collectively, the seminar assembled expertise in diverse synthesis techniques and application areas.

The first half of the seminar focused on educating the participants in foundations and empirical results developed over the last three decades in the mostly isolated synthesis communities. The seminar started with tutorial talks on deductive synthesis, controller synthesis, inductive synthesis, and the use of decision procedures in program synthesis. The second half of the seminar led to a lot of discussion, boosted by talks on specific software synthesis problems.

The participants agreed that there are several reasons to actively explore synthesis now. First, software development, always non-trivial, is likely to become more complicated as a result of transition to multi-core processors. The hope is that we will synthesize at least the hard fragments of parallel programs. Second, deductive program verification and synthesis are intimately related; it seems promising to explore whether results in model checking and directed testing enable interesting synthesis. Third, by incorporating verification into synthesis we may be able to synthesize programs that are easier to verify than handwritten programs. Finally, the continuing Moore's Law may enable search powerful enough for synthesis of practical programs.

The seminar also led to identification of principles and open problems in benchmarking of software synthesis tools. In contrast to benchmarking of compilers and verifiers, experiments with synthesis must evaluate end-to-end benefits in programmer productivity; in particular, can the program be developed faster with the synthesizer than with a modern programming language? Short of performing a controlled user study, little can be said about the magnitude of these benefits. The situation is more favorable when comparing synthesis tools. The participants agreed that experiments reported in the literature must identify the knowledge that the user had to formalize in the domain theory that made the synthesis possible. It was also deemed important to identify the formalism used in expressing the domain knowledge.

General Conclusions from the Seminar. The participants found the seminar to be educational and inspiring. We believe this was because of the unusual breadth of participants as well as the format, which revolved around tutorial-style talks that brought the participating communities together.

The participants believed that the talks should be shared with graduate students, who are usually exposed in their courses only to a fraction of synthesis techniques. This observation led to organization of summer school on synthesis, which will be held in Dagstuhl in summer 2011.

The need to create a collection of diverse synthesis results also led to a special issue of the STTT journal of software synthesis, which is under preparation.

In Memoriam

We are very sad to learn that Prof. Amir Pnueli passed suddenly away on Nov. 2nd, 2009
Obituary of The New York University
www.cs.nyu.edu/csweb/People/amirpnueli.html