Home
Lehre
aktuelle Semester...
Sommersemester 18
Wintersemester 17/18
Personen
Research
Projects
Events
Jobs/Studienarbeiten
SiteMap
Puma
Impressum & Datenschutz
|
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
|