- Offered in: Fall 2019
- Time: TBD
- Instructors: Karim Ali
- Spencer Killen
Program synthesize strives to automatically create programs that satisfy a high-level, possibly incomplete, specifications. This course covers the foundations of program synthesis, including methods of program specification, SAT solvers, and program verification in addition to following methods of program synthesis:
- Inductive Synthesis (Including counterexample-guided inductive synthesis)
- Deductive Synthesis
- Superoptimization
- Program Sketching
- And Oracle-guided synthesis
The student will review literature and study advancements in the field. The second half of the course is oriented towards creating a project which demonstrates and practicalizes the student's learnings.
- Class Presentations: 30%
- Assignments: 20%
- Practical Experiments: 20%
- Final Report: 30%
| Duration | Activity | Details |
|---|---|---|
| Sep 03 - Oct 12 | Literature Review | Weekly meetings for presentation/discussion of papers. Students will explore existing tools for program synthesis and will execute at least one programming assignment using one or multiple tools so that they can understand the advantages and shortcomings of each tool. |
| Oct 11 | Project Proposal | 1-page written proposal + presentation to the instructor. |
| Oct 11 - Dec 5 | Tool improvements and formulation of research problems | Weekly meetings to review tool designs, specify improvements and formulate potential research problems. |
| Dec 6 | Final project presentation and report | 30 minute presentation + a written conference-style report. |
- Behavioral Program Synthesis with Genetic Programming 2016 (Krawiec, Krzysztof) Book
- Program Synthesis 2017 (Gulwani, Oleksandr Polozov, Rishabh Singh) Book
- Logic Program Synthesis from Incomplete Information 2012 (Flener) Book
- Program Sythesis 2018 (Polozov) Blog
- Program Sythesis in 2019 (Bornholt) Blog
- Program Synthesis Without Full Specifications for Novel Applications 2015 (Perelman) Dissertation
- Program Synthesis by Sketching 2003 (Solar-Lezama) Dissertation
- Microsoft Program Synthesis 2010- (Gulwani) Research hub
- Constraint-Based Synthesis of Datalog Programs 2017 (Albarghouthi, Koutris, Nai, Smith) Conference paper
- Syntax-guided synthesis 2013 (Alur, Bodik, Juniwal, Martin, Raghothaman, Seshia, Singh, Solar,-Lezama, Torlak, Udupa) Conference paper
- Language to Specify Syntax-Guided Synthesis Problems 2017 (Raghothaman, Udupa) Article
- The Sketching Approach to Program Synthesis 2009 (Solar-Lezama) Conference paper
- Program Synthesis for Hierarchical Specifications 2014 (Hottelier, Bodik) Conference paper
- Type-and-example-directed program synthesis 2015 (Osera, Zdancewic) Conference paper PLDI
- A lightweight symbolic virtual machine for solver-aided host languages 2014 (Torlak, Bodik) Conference paper PLDI