Lehrstuhl Informatik II   
Sprachen und Beschreibungsstrukturen      
   Home Lehre Sommersemester 18 Seminare Program Synthesis login

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 sketchingInt 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 superoptimizationASPLOS'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 ProgrammingICSE '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 ExamplesVLDB Endowment'12
Genetic programming Lucas Mair van Berkel, Turi, Pruteanu, Dulman Automatic Discovery of Algorithms for Multi-Agent Systems, GECCO'12

Survey papers:

  1. R.Bodik, B.Jobstmann Algorithmic program synthesis: introduction,Int J Softw Tools Technol Transfer (2013)
  2. 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. 

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


TUM - Lehrstuhl Informatik II (Sprachen und Beschreibungsstrukturen) Thanks: Tango and TinyMCE     Generationszeit: 15 ms