Trends in Software Synthesis

Seminar (7 CP)
WS 2015/16


Bernd Finkbeiner
Swen Jacobs
Hazem Torfah

News

Topic

Program synthesis in its classical formulation is concerned about finding a program that meets a specification given as a logical formula. Recent work on program verification and program optimization have shown potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations.

In this seminar we look into various novel approaches in program synthesis. The topics will be divided mainly into three categories. Deductive Synthesis, where synthesis is regarded as a theorem proving task, syntax-guided synthesis, where a partial program with incomplete information is completed using user-specified assertions and finally, learning-based approaches, where the synthesis procedure is formulated as a learning algorithm between an oracle and the synthesizer.

The seminar is split into two parts. The first part will take the form of reading sessions, where we lay the foundations of the topic. The second part will consist of presentations about recent papers from the three categories mentioned above.