|Dozent:||Anastasiia Izycheva, Raphaela Palenta|
|Ort/Zeit:||Room 02.07.053 - 1-1 meetings|
|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.
Upcoming week and deliverables are marked bold in the table.
Schedule for the final presentations is here.
||April 9 - 15
||Kick-off meeting, choose the topic
||April 16 - 22
||Find related work papers
|| April 22, 23:59
||List of papers you are going to work with
||April 23 - May 6
||Review of paper 1
|| May 6, 23:59
||PDF-file with the review - paper 1
||May 7 - 20
||Review of paper 2
|| May 20, 23:59
||PDF-file with the review - paper 2
||May 21 - June 3
||Review of paper 3
|| June 3, 23:59
||PDF-file with the review - paper 3
||June 4 - 17
||Prepare the final presentation. Present your project
June 15th 10.00 - 18.00 (roughly estimated). Room 02.07.034
||June 18 - July 1
||Write a final report on your project
|| July 1, 23:59
||PDF-file with your final report
||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
| Type-based synthesis
||Michael Benedikt Schwarz
||Polikarpova, Kuraj, Solar-Lezama Program Synthesis from Polymorphic Refinement Types, PLDI'16
| Enumerative synthesis
||Rajeev, Radhakrishna, Udupa Scaling Enumerative Synthesis via Divide and Conquer, TACAS'17
| Counter-example guided synthesis
||Solar-Lezama Program sketching, Int J Softw Tools Technol Transfer (2013)
| Proof-based synthesis
||Kuncak, Mayer, Piskac, Suter Complete Functional Synthesis, PLDI'10 or Software Synthesis Procedures, Communications of ACM (Feb 2012)
| Machine learning algorithms
||Raychev, Bielik, Vechev Probabilistic Model for Code with Decision Trees, OOPSLA'16
| Program repair
||Rolim, Soares, D'Antoni, Polozov, Gulwani, Gheyi, Suzuki, Hartmann Learning syntactic program transformations from examples, ICSE'17
||Schkufza, Sharma, Aiken Stochastic superoptimization, ASPLOS'13 or Stochastic Optimization of Floating-Point Programs with Tunable Precision, PLDI'14
| Database algorithms
||Yaghmazadeh, Wang, I.Dillig, T.Dillig SQLizer: Query Synthesis from Natural Language, OOPSLA'17
| Data structures
||Etienne Kneuss, Viktor Kuncak, Ivan Kuraj, Philippe Suter Synthesis Modulo Recursive Functions, OOPSLA'13
||Weimer, Nguyen, Le Goues, Forrest Automatically Finding Patches Using Genetic Programming, ICSE '09
| Program Understanding
||Raychev, Vechev, Krause Predicting Program Properties from “Big Code”, POPL'15
| String-manipulation funcitons
||Singh, Gulwani Learning Semantic String Transformations from Examples, VLDB Endowment'12
||van Berkel, Turi, Pruteanu, Dulman Automatic Discovery of Algorithms for Multi-Agent Systems, GECCO'12
- 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.
- 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