263-2910-00L Program Analysis and Synthesis
| Semester | Spring Semester 2016 |
| Lecturers | M. Vechev |
| Periodicity | yearly course |
| Language of instruction | English |
Catalogue data
| Abstract | This course covers modern automated program analysis and synthesis techniques, including: (i) core theoretical foundations, and (ii) applications of these foundations for solving useful practical challenges. The techniques are widely applicable and are increasingly being used in a wide range of areas (e.g., systems, networks, security, etc). |
| Objective | The course has 4 main objectives: * Understand the foundational principles behind modern automated program analysis and synthesis techniques. * Understand how to apply these principles to build practical, working systems that can solve interesting real-world problems. * Understand how these techniques interface with other research areas (e.g., machine learning, security) * Gain familiarity with state-of-the-art in the area and with future research 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, networks) to automating the construction of programs (e.g., for end user programming) and machine learning models (e.g., probabilistic programming). This course will provide a comprehensive introduction to modern, state-of-the-art program analysis and synthesis concepts, principles and research trends, including: * Static Analysis: - concepts: approximation, domains, precision, fixed points, numerical and heap analysis, asymptotic complexity, performance optimizations - frameworks: APRON, PPL, ELINA, Facebook's Flow, Soot, LLVM, WALA * Probabilistic programs and analysis - concepts: Baysean networks, probabilistic languages (e.g., R2, Stan) - frameworks: Alchemy, Markov Logic Networks, Picture * Modern program synthesis (e.g. programming from examples for end users): - concepts: L*, version spaces, Programming by Example, CEGIS - frameworks: Sketch, AGS, SmartEdit, ReSynth, Flashfill * Learning-based program synthesis: - concepts: Markov networks, generative / discriminative models, probabilistic grammars - frameworks: Nice2Predict * Learning-based program analysis - concepts: language models, neural networks - frameworks: SLANG, JSNice (http://jsnice.org) * Dynamic Analysis: - concepts: soundness, efficiency, complexity, stateless model checking - frameworks: FastTrack, EventRacer, Chess * Predicate abstraction: - concepts: Graf-Saidi, Boolean programs, lazy abstraction - frameworks: Microsoft's SLAM, BLAST, Fender * Symbolic execution: - concepts: SMT, concolic execution - frameworks: S2E, KLEE, Sage * Security Analysis: - concepts: information flow, hyperproperties - example: malware detection * Applications of Analysis & Synthesis: - finding security violations in web and mobile applications (e.g., JavaScript, Android), establishing properties of biological systems (e.g. DNA computation), analysis of systems software (e.g. , drivers, software defined networks), discovery of new algorithms (e.g. concurrent data structures, distributed algorithms), automating end-user programming, automating probabilistic inference (e.g. Intel's x86, ARM), and others. To gain a deeper understanding of how to apply these techniques in practice, the course will involve a hands-on programming project where based on the principles introduced in class, the students will build an analysis / synthesis system. |
| 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. |
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 |
| M. Vechev | |||
| 263-2910-00 U | Program Analysis and Synthesis | 2 hrs |
| 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 |  |
| Computer Science Master | Focus Core Courses Software Engineering | W | |