SC5404 INTRODUCTION TO PROGRAM SYNTHESIS

This course aims to give an introduction to program synthesis, an exciting 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 generate programs that do what the user wants. In particular, the class will explore the following questions: 1. The intention question: 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 ambiguous or incomplete? 2. Interplay between program search and program verification: how do we ensure that the program we synthesize will actually be deemed correct by a potentially brittle verification mechanism, and how do we use a verifier to our advantage to help synthesize programs faster? 3. Interplay between program synthesis and deep learning: how do you reconcile the symbolic techniques traditionally used for synthesis and verification with deep learning? We will explore learning based techniques including language models based on transformers and reinforcement learning. 4. Program synthesis beyond software engineering: the course will also discuss applications of program synthesis beyond automated programming to other domains where one has to generalize from small number of examples and produce interpretable models, as well as neurosymbolic learning techniques that combine ideas from program synthesis with ML.