263-2910-00L  Program Analysis and Synthesis

SemesterSpring Semester 2017
LecturersM. Vechev
Periodicityyearly course
Language of instructionEnglish

Catalogue data

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., http://jsnice.org, http://apk-deguard.com)

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.

Performance assessment

Performance assessment information (valid until the course unit is held again)
Performance assessment as a semester course
ECTS credits6 credits
ExaminersM. Vechev
Typesession examination
Language of examinationEnglish
Course attendance confirmation requiredNo
RepetitionThe performance assessment is only offered in the session after the course unit. Repetition only possible after re-enrolling.
Mode of examinationoral 20 minutes
Additional information on mode of examinationThe grade will be determined by one semester-long project with final report and presentation (50%) + an oral exam (50%).
This information can be updated until the beginning of the semester; information on the examination timetable is binding.

Learning materials

Main linkInformation
Only public learning materials are listed.


263-2910-00 VProgram Analysis and Synthesis3 hrs
Mon13-16CAB G 51 »
M. Vechev
263-2910-00 UProgram Analysis and Synthesis2 hrs
Tue13-15CHN F 46 »
M. Vechev


There are no additional restrictions for the registration.

Offered in

Certificate of Advanced Studies in Computer ScienceFocus Courses and ElectivesWInformation
Computer Science MasterFocus Core Courses Software EngineeringWInformation