263-2910-00L  Program Analysis and Synthesis

SemesterSpring Semester 2017
LecturersM. Vechev
Periodicityyearly recurring course
Language of instructionEnglish


AbstractThis course covers the theory and practice of modern automated program analysis and synthesis, including both, discrete and probabilistic programs.

The techniques discussed in the course are general and widely applicable to problems in software engineering and verification, security, networks, machine learning, and other areas.
Objective* Understand the foundations of automated program analysis and synthesis techniques, including standard (discrete) and probabilistic programs.

* Understand how these foundations are applied to solve practical real-world problems.

* Understand how to interface these methods to other research areas (e.g., deep learning, Bayesian inference, security, networks)

* Understand the state-of-the-art in the area and future trends.
ContentThe last decade has seen an explosion in modern program analysis and synthesis techniques. These techniques are increasingly being used to reason about a vast range of computational paradigms, from finding security flaws in systems software (e.g., drivers) to automating the construction of programs (e.g., for end user programming), to programmable networks, to reliable machine learning models (e.g., probabilistic programming). This course provides a comprehensive introduction to these methods.

The course consists of 3 parts:

* Part I: Theory and Practice of Static Analysis

Static analysis is the science of creating precise and scalable finite approximations of potentially infinite behaviors so to enable a machine to automatically reason about these. These behaviors may come from programs but also other dynamic systems (e.g., biological). Hence the theory and principles of static analysis are widely applicable. We will cover:

- concepts: abstract interpretation, abstract domains, precision vs. asymptotic complexity
- applications: JavaScript type checking (as in Facebook's Flow), security analysis, parallelism and concurrency reasoning (e.g., GPU, weak memory).

* Part II: Theory and Practice of Synthesis

Modern program synthesis is an approach for automating the construction of programs from (partial) user intent. Recent years have seen exciting breakthroughs in techniques and algorithms that discover complex programs purely from input/output examples, natural language, partial programs (sketches) and many others forms of supervision and intent. Modern program synthesis can be seen as a path towards the ultimate goal of artificial intelligence and explainable machine learning. We will cover:

- concepts: version spaces, counter-example guided inductive synthesis, SMT solvers.
- applications: programming by example (e.g., Microsoft's FlashFill), programmable networks (e.g., SyNet).

* Part III: Programming Languages (PL) and Machine Learning (ML)

We will cover the latest and most exciting developments bridging the areas of machine learning and programming languages. These trends include both directions: (i) PL techniques applied to ML problems, and (ii) ML techniques applies to PL tasks (e.g., reasoning about a program). Here, we will cover:

- concepts: probabilistic programming, neural program synthesis (e.g., advance neural networks such as Neural Turing Machines), program synthesis with noise.
- applications: approximate computing, learning-based probabilistic programming engines (e.g., Link, Link)


To gain a deeper understanding of how to apply these techniques, the course will also involve a hands-on programming project.
Lecture notesThe lectures notes will be distributed in class.
LiteratureDistributed in class.
Prerequisites / NoticeThis course is aimed at both graduate (M.Sc., PhD) students as well as advanced undergraduate students.

The course has an oral exam, but for those on summer internships, the exam can be moved to the end of the semester.