263-2910-00L  Program Analysis and Synthesis

Semester Spring Semester 2017
Lecturers M. Vechev
Periodicity yearly course
Language of instruction English



Catalogue data

Abstract This 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.
Content The 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 notes The lectures notes will be distributed in class.
Literature Distributed in class.
Prerequisites / Notice This 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 credits 6 credits
Examiners M. Vechev
Type session examination
Language of examination English
Course attendance confirmation required No
Repetition The performance assessment is only offered in the session after the course unit. Repetition only possible after re-enrolling.
Mode of examination oral 20 minutes
Additional information on mode of examination The 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 link Information
Only public learning materials are listed.

Courses

Number Title Hours Lecturers
263-2910-00 V Program Analysis and Synthesis 3 hrs
Mon 13-16 CAB G 51 »
M. Vechev
263-2910-00 U Program Analysis and Synthesis 2 hrs
Tue 13-15 CHN F 46 »
M. Vechev

Restrictions

There are no additional restrictions for the registration.

Offered in

Programme Section Type
Certificate of Advanced Studies in Computer Science Focus Courses and Electives W Information
Computer Science Master Focus Core Courses Software Engineering W Information