The goal of this course is to give an introduction to program synthesis, a new field at the intersection of programming languages, formal methods, and AI. The course will explore a number of fundamental questions around the problem of how to automatically discover programs that do what the user expects. The workloads include 2~3 programming assignments, 4~5 paper reviews, and a final project. In particular, the class will explore the following questions:
User intent: How does the user convey intent and how do we increase the likelihood that the synthesizer will produce the desired program even when the specification is incomplete?
The interplay between program search and program verification: how do we ensure that the program we synthesize will be correct, and how do we use a verifier to speed up the synthesizer?
We will explore this question in the context of attack synthesis and exploit generation.
The interplay between program synthesis and deep learning: how do we reconcile the symbolic reasoning techniques with deep learning? We will explore this question in the context of data visualization and data science.
Prerequisite: CMPSC 40 with a grade of C or better, or Math 8 with a grade of C or better.