Dagstuhl Seminar 09501
( Dec 06 – Dec 11, 2009 )
- Rastislav Bodik (University of California - Berkeley, US)
- Orna Kupferman (The Hebrew University of Jerusalem, IL)
- Douglas R. Smith (Kestrel Institute, US)
- Eran Yahav (IBM TJ Watson Research Center - Hawthorne, US)
- Annette Beyer (for administrative matters)
- Synthesis : Special Issue - Bodik, Rastislav; Jobstmann, Barbara - Berlin : Springer, 2013 - (International Journal on Software Tools for Technology Transfer : 15. 2013, 5/6).
- Synthesis for regular specifications over unbounded domains : article pp. 101-109 : FMCAD 2010, Formal Methods in Computer-Aided Design 2010 - Hamza, Jad; Jobstmann, Barbara; Kuncak, Viktor - Los Alamitos : IEEE, 2010. - pp. 101-109.
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.
We are very sad to learn that Prof. Amir Pnueli passed suddenly away on Nov. 2nd, 2009
Obituary of The New York University
- Rastislav Bodik (University of California - Berkeley, US) [dblp]
- Satish Chandra (IBM TJ Watson Research Center - Yorktown Heights, US) [dblp]
- Ewen W. Denney (NASA - Moffett Field, US) [dblp]
- Bernd Finkbeiner (Universität des Saarlandes, DE) [dblp]
- Sumit Gulwani (Microsoft Corporation - Redmond, US) [dblp]
- Ashutosh Kumar Gupta (MPI-SWS - Saarbrücken, DE)
- Shachar Itzhaky (Tel Aviv University, IL)
- Barbara Jobstmann (VERIMAG - Grenoble, FR) [dblp]
- Joost-Pieter Katoen (RWTH Aachen, DE) [dblp]
- Uri Klein (New York University, US)
- Viktor Kuncak (EPFL - Lausanne, CH) [dblp]
- Martin Leucker (TU München, DE) [dblp]
- Yanhong Annie Liu (SUNY - Stony Brook, US)
- Doron A. Peled (Bar-Ilan University - Ramat Gan, IL) [dblp]
- Nir Piterman (Imperial College London, GB) [dblp]
- Andreas Raabe (fortiss GmbH - München, DE)
- Andrey Rybalchenko (MPI-SWS - Saarbrücken, DE) [dblp]
- Sven Schewe (University of Liverpool, GB) [dblp]
- Johann M. Schumann (NASA - Moffett Field, US)
- Douglas R. Smith (Kestrel Institute, US)
- Armando Solar-Lezama (MIT - Cambridge, US) [dblp]
- Saurabh Srivastava (University of Maryland - College Park, US) [dblp]
- Martin Vechev (IBM TJ Watson Research Center - Yorktown Heights, US) [dblp]
- Richard Waldinger (SRI - Menlo Park, US)
- Eran Yahav (IBM TJ Watson Research Center - Hawthorne, US) [dblp]
- Greta Yorsh (IBM TJ Watson Research Center - Yorktown Heights, US) [dblp]
- Dagstuhl Seminar 12152: Software Synthesis (2012-04-09 - 2012-04-13) (Details)
- programming languages / compilers
- verification / logic
- software synthesis
- Software Synthesis
- Theorem Proving
- Program Analysis
- Programming by Demonstration