TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 12152

Software Synthesis

( 09. Apr – 13. Apr, 2012 )

(zum Vergrößern in der Bildmitte klicken)

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/12152

Organisatoren
  • Rastislav Bodik (University of California - Berkeley, US)
  • Sumit Gulwani (Microsoft Corporation - Redmond, US)
  • Eran Yahav (Technion - Haifa, IL)

Kontakt


Summary

Software verification and synthesis are founded on similar principles, yet verification has become industrial reality while successes of synthesis remain confined to a handful of domains. Still, recent years witnessed increased interest in software synthesis---a trend spurred by growing software complexity and simultaneously enabled by advances in verification, decision procedures, and machine learning. The goal of the seminar is to help the revival of software synthesis through intellectual exchange among experts in deductive synthesis, controller synthesis and the diverse spectrum of new synthesis efforts in inductive synthesis, auto-tuning, programming by demonstration and partial programming. This is an opportune moment for software synthesis. First, multi-core processors are likely to make software development harder, motivating automatic construction of synchronization and communication code. Second, software verification and checking reached industrial maturity through judicious use of linguistic support, decision procedures, and dynamic analyses, inspiring solutions to open synthesis problems. Third, by incorporating verification into synthesis, we may be able to synthesize programs that are easier to verify than handwritten programs. Fourth, parallel computers enable search powerful enough for synthesis of well-tuned programs, as demonstrated by auto-tuners and super-optimizers. Finally, recent systems built on programming by demonstration make us hope that specification will be easier to write.

The seminar organizers hope to achieve the following goals:

  • Offer brief tutorials on techniques developed by communities participating in the seminar.
  • Develop a set of challenge problems for practical synthesis, a collection of practical problems solvable by (semi-)automatic synthesis in five years.
  • Deepen the understanding of the relationships between the various approaches to synthesis. In particular, to what extent are the techniques developed by the respective communities independent from their driving applications? Understand strengths of the alternative approaches.
  • Understand relationships and applicability of verification technology to software synthesis.
  • Outline a syllabus for a graduate course in software synthesis.

Teilnehmer
  • Rajeev Alur (University of Pennsylvania - Philadelphia, US) [dblp]
  • Don Batory (University of Texas - Austin, US) [dblp]
  • Rastislav Bodik (University of California - Berkeley, US) [dblp]
  • Krzysztof Czarnecki (University of Waterloo, CA) [dblp]
  • Jyotirmoy Deshmukh (University of Pennsylvania - Philadelphia, US) [dblp]
  • Laurent Doyen (ENS - Cachan, FR) [dblp]
  • Bernd Finkbeiner (Universität des Saarlandes, DE) [dblp]
  • Pierre Flener (Uppsala University, SE) [dblp]
  • Franz Franchetti (Carnegie Mellon University, US) [dblp]
  • Sumit Gulwani (Microsoft Corporation - Redmond, US) [dblp]
  • Amey Karkare (Indian Institute of Technology - Kanpur, IN)
  • Hadas Kress-Gazit (Cornell University, US) [dblp]
  • Vu Le (University of California - Davis, US) [dblp]
  • Rupak Majumdar (MPI-SWS - Kaiserslautern, DE) [dblp]
  • Oded Maler (VERIMAG - Grenoble, FR) [dblp]
  • Mark Marron (IMDEA Software - Madrid, ES) [dblp]
  • Alon Mishne (Technion - Haifa, IL)
  • Jean-Noël Monette (Uppsala University, SE)
  • Georg Ofenbeck (ETH Zürich, CH) [dblp]
  • Doron A. Peled (Bar-Ilan University - Ramat Gan, IL) [dblp]
  • Ruzica Piskac (MPI-SWS - Saarbrücken, DE) [dblp]
  • Nir Piterman (University of Leicester, GB) [dblp]
  • Corneliu Popeea (TU München, DE)
  • Subhajit Roy (Indian Institute of Technology - Kanpur, IN) [dblp]
  • Roopsha Samanta (University of Texas - Austin, US) [dblp]
  • Sven Schewe (University of Liverpool, GB) [dblp]
  • Sanjit A. Seshia (University of California - Berkeley, US) [dblp]
  • Armando Solar-Lezama (MIT - Cambridge, US) [dblp]
  • Saurabh Srivastava (University of California - Berkeley, US) [dblp]
  • Philippe Suter (EPFL - Lausanne, CH)
  • Nathalie Sznajder (UPMC - Paris, FR)
  • Emina Torlak (University of California - Berkeley, US) [dblp]
  • Stavros Tripakis (University of California - Berkeley, US) [dblp]
  • Martin Vechev (ETH Zürich, CH) [dblp]
  • Christian von Essen (VERIMAG - Grenoble, FR)
  • Eran Yahav (Technion - Haifa, IL) [dblp]
  • Jean Yang (MIT - Cambridge, US) [dblp]

Verwandte Seminare
  • Dagstuhl-Seminar 09501: Software Synthesis (2009-12-06 - 2009-12-11) (Details)

Klassifikation
  • program synthesis: linguistic support for specifications and programmer-tool interaction
  • algorithmics
  • applications

Schlagworte
  • Software Synthesis
  • Verification and Model Checking
  • Theorem Proving
  • Program Analysis
  • Programming by Demonstration
  • Program Derivation
  • Compiler Optimization