About This Course
The goal of program synthesis is to automatically find a program that satisfies the user intent expressed in the form of some specification.
Program synthesis stands at the intersection of multiple disciplines, programming languages, artificial intelligence and data science.This course gives an introduction to the field, and requires the students to learn about the state-of-the-art by reading recent articles and working on a course project.
Learning Objectives
The topics we plan to cover include inductive, functional, counter-example guided and type-driven synthesis.
Reading Material
- There is no required textbook for this course. Students require to read the relevant papers introduced during the course.
- Some materials of this course have been borrowed from the similar course given by Armando Solar-Lezama.
Schedule
| Date | Lecture | |
| 1 | 2 Esfand | Course Overview |
| 2 | 4 Esfand | Introduction to Inductive Synthesis |
| 3 | 9 Esfand | Bottom-Up Enumerative Search |
| 4 | 11 Esfand | Top-Down Enumerative Search |
| 5 | 16 Esfand | Statistical Models in Synthesis |
| 6 | 18 Esfand | Stochastic Search |
| 7 | 23 Esfand | Representation-based search |
| 25 Esfand | How to give a great research talk (Simon Peyton Jones) | |
| 8 | 14 Farvardin | Boolean Satisfiability (SAT) Solving |
| 9 | 16 Farvardin | Satisfiability Modulo Theories |
| 21 Farvardin | Class Presentation: Papers (1) | |
| 10 | 23 Farvardin | Constraint-based Search |
| 11 | 28 Farvardin | Constraint-based Synthesis with Sketch (1) |
| 12 | 30 Farvardin | Constraint-based Synthesis with Sketch (2) |
| 4 Ordibehesht | Class Presentation: Papers (2) | |
| 13 | 6 Ordibehesht | Introduction to Functional Synthesis |
| 11 Ordibehesht | Class Presentation: Project Progress Report | |
| 14 | 13 Ordibehesht | Proving Program Correctness |
| 18 Ordibehesht | Tutoring Session (Program Verification) | |
| 15 | 20 Ordibehesht | From Verification to Synthesis |
| 25 Ordibehesht | Class Presentation: Papers (3) | |
| 16 | 27 Ordibehesht | Expressive Types |
| 17 | 1 Khordad | Synthesis with Refinement Types |
| 18 | 3 Khordad | Deductive Synthesis |
| 19 | 8 Khordad | Synthesis for Data Science |
| 10 Khordad | Class Presentation: Papers (4) | |
| 20 | 17 Khordad | Guest Lecture: Prof. Sirjani (Research) |
| 22 Khordad | Class Presentation: Papers (5) | |
| 21 | 24 Khordad | Model Learning |
| 22 | 29 Khordad | Guest Lecture: Prof. Mousavi (Research) |
| 23 | 31 Khordad | Network Synthesis (Research) |
Marking Criteria
- 20% Paper review and presentation
- 20% Project
- 60% Final Exam