Program Synthesis

Dozent:	Anastasiia Izycheva
Ort/Zeit:	Room 02.07.053 - 1-1 meetings
ModulNummer:	IN0014, IN2107
Beschreibung:	During the seminar we will touch the surface of the current research on program synthesis. We will see several applications and learn about techniques used to generate code automatically.

UPD: All submissions are done by email. Please only send me PDF file with your review.

The template for reviews is available here. ACM Proceedings latex style is most likely already installed on your computer, but in case you're missing here is class file and bibstyle file.

-----------------------------

Who: Master Students, advanced Bachelor students are welcome as well.

Language: The seminar will be held in English.

Prerequisites: There are no formal prerequisites, but the words "formal methods", "verification", "search space" etc. should not scare you but rather inspire :)

Grading: Your final grade will be based on the four submitted reviews, final presentation and report. For contribution of each part in percentage see the table below.

The seminar involves reading, summarising, reviewing and analysing research papers. If you haven't done that before, no worries, I will give you some hints on how to proceed.

Schedule

Upcoming week and deliverables are marked bold in the table.

week #	Dates	Activity	Deadline	Deliverables	Grading
1	April 9 - 15	Kick-off meeting, choose the topic	-	Topic preferences	-
2	April 16 - 22	Find related work papers	April 22, 23:59	List of papers you are going to work with	bonus
3-4	April 23 - May 6	Review of paper 1	May 6, 23:59	PDF-file with the review - paper 1	10%
5-6	May 7 - 20	Review of paper 2	May 20, 23:59	PDF-file with the review - paper 2	10%
7-8	May 21 - June 3	Review of paper 3	June 3, 23:59	PDF-file with the review - paper 3	10%
9-10	June 4 - 17	Prepare the final presentation. Present your project	Presentation day, probably June 15	Project presentations, exact dates TBA	30%
11-12	June 18 - July 1	Write a final report on your project	July 1, 23:59	PDF-file with your final report	30%
13-14	July 2 - 15	Review an assigned final report of your classmate. Be kind and constructive!	July 15, 23:59	PDF-file with the review - classmate's project	10%

Topic assignment

Topic	Student	Paper 1
By technique
Type-based synthesis	Michael Benedikt Schwarz	Polikarpova, Kuraj, Solar-Lezama Program Synthesis from Polymorphic Refinement Types, PLDI'16
Enumerative synthesis	Fritz Lumnitz	Rajeev, Radhakrishna, Udupa Scaling Enumerative Synthesis via Divide and Conquer, TACAS'17
Counter-example guided synthesis	Florian Stamer	Solar-Lezama Program sketching, Int J Softw Tools Technol Transfer (2013)
Proof-based synthesis	Paul Bachmann	Kuncak, Mayer, Piskac, Suter Complete Functional Synthesis, PLDI'10 or Software Synthesis Procedures, Communications of ACM (Feb 2012)
Machine learning algorithms	Manuel Bildhauer	Raychev, Bielik, Vechev Probabilistic Model for Code with Decision Trees, OOPSLA'16

By application
Program repair	Tobias Schmidt	Rolim, Soares, D'Antoni, Polozov, Gulwani, Gheyi, Suzuki, Hartmann Learning syntactic program transformations from examples, ICSE'17
Superoptimization	Levon Oganyan	Schkufza, Sharma, Aiken Stochastic superoptimization, ASPLOS'13 or Stochastic Optimization of Floating-Point Programs with Tunable Precision, PLDI'14
Database algorithms	Alexander Roschlaub	Yaghmazadeh, Wang, I.Dillig, T.Dillig SQLizer: Query Synthesis from Natural Language, OOPSLA'17
Data structures	Julian Dräger	Etienne Kneuss, Viktor Kuncak, Ivan Kuraj, Philippe Suter Synthesis Modulo Recursive Functions, OOPSLA'13
Debugging	Sebastian Kaster	Weimer, Nguyen, Le Goues, Forrest Automatically Finding Patches Using Genetic Programming, ICSE '09
Program Understanding	Monika Semwal	Raychev, Vechev, Krause Predicting Program Properties from “Big Code”, POPL'15
String-manipulation funcitons	Markus Webel	Singh, Gulwani Learning Semantic String Transformations from Examples, VLDB Endowment'12
Genetic programming	Lucas Mair	van Berkel, Turi, Pruteanu, Dulman Automatic Discovery of Algorithms for Multi-Agent Systems, GECCO'12

Survey papers:

R.Bodik, B.Jobstmann Algorithmic program synthesis: introduction,Int J Softw Tools Technol Transfer (2013)
Gulwani Dimensions in Program Synthesis, PPDP'10

These papers are optional, but I recommend to have a look at them.

Helpful resources:

I expect all of you to have some background in verification, but if you need a recap/help here is a nice source. It's a syllabus of a course in CMU, no need to read it completely, but feel free to read the parts relevant for your topic.
The inforgraphic on how to read a scientific paper.
Slides from the kick-off meeting

Here is the list of topics that were not assigned, but I keep the papers here just for reference.

Constraint-based learning - Gulwani, Jha, Tiwari, Venkatesan Synthesis of Loop-free Programs, PLDI'11
Version-space algebra (by demonstration) - Gulwani Automating string processing in spreadsheets using input-output examples, POPL'11
Quantitative synthesis - Bornholt, Torlak, Grossman, Ceze Optimizing Synthesis with Metasketches, POPL'16