| Instructor | Eva Darulova |
| TA | Soham Chakraborty |
| Time | Tuesdays, 14:15 - 16:00 |
| Place | SB building E1.5 room 029, videocast to KL building G 26 room 607 |
| First meeting | 10 April |
| Office hours | On demand, send an email to Eva |
| Credits | 7 CP |
| Prerequisites | No formal requirements, but prior experience with program analysis, verification or automated reasoning is helpful. |
| Can I audit? | Yes |
The idea that we could tell a computer what we want and it would automatically figure out how to achieve it has fascinated scientists for a long time, but it has also been an elusive goal. Via recent research papers in the area of program synthesis, this seminar will look at the significant steps which have been made towards this grand vision. We will discuss what is currently possible, for which application domains program synthesis is successful, what the main challenges are and what perhaps will never be feasible. The paper selection will cover the major synthesis techniques to provide an overview of the current landscape.
Disclaimer: The name 'synthesis' can mean many different things, in particular there are two different areas whose goal is to generate programs. This course considers the often so-called functional synthesis which aims to synthesize programs whose inputs are finite, e.g. a sorting algorithm. On the other hand, the input of reactive synthesis generated programs are infinite streams, e.g. in embedded controllers. This introduction nicely explains the differences and also provides an introduction to program synthesis. The approaches in these two domains are quite different, and in this seminar we will focus on functional synthesis.
| Format | This seminar will follow a regular structure: every registred student is assigned one recent research paper, which he/she presents during the class. In addition, students prepare a (brief) report, which summarizes the main aspects of the techniques surveyed during the semester. |
| Registration |
If you are interested to take this seminar for credit,
fill in this registration form by 30 March. Places in the seminar are limited, but places for non-credit participants are unlimited. |
| Paper Assignment | will be done in the first week based on students' preferences. |
| Grading | The final grade will be based on the paper presentation, participation in class, as well as the final summary report. |
| Course platform | We will use Moodle for course coordination and communication, thus all participants, even those only auditing the class should register on Moodle. The enrollment method will be announced at the first class. |
| Following from KL | Following this seminar from Kaiserslautern is possible; we will have the discussion sessions videocast. However, for students wanting to take this seminr for credit, it is advised if they can attend at least some of the sessions in persion in Saarbrücken. |