Program Synthesis

Dozent:	Anastasiia Izycheva, Raphaela Palenta
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.

Template for the final report is here, it also contains some instructions. UPDATED grading rubrics for the final report are here.

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

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.

Template for the review is 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.

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

Schedule

Upcoming week and deliverables are marked bold in the table.

Schedule for the final presentations is here.

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, June 15	Project presentations, June 15th 10.00 - 18.00 (roughly estimated). Room 02.07.034	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
Grading rubrics for presentations

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