263-2910-00L  Program Analysis

Semester Autumn Semester 2013
Lecturers M. Vechev
Periodicity yearly course
Language of instruction English



Catalogue data

Abstract The principles of modern program analysis are key to enabling scalable and automated reasoning for a vast range of computations (e.g. mobile app security, high-performance algorithms, biological computing, device drivers).

This course is an in-depth introduction to the fundamental principles and applications of modern program analysis.

For more information: http://www.srl.inf.ethz.ch/pa.php
Objective The course has 3 main objectives:

* Understand the foundational principles behind program analysis techniques.

* Understand how to apply these principles to build practical, working analyzers. This will be helped by a hands-on programming project.

* Gain familiarity with the state-of-the-art in the research area.
Content The last decade has seen an explosion in modern program analysis techniques. These techniques are increasingly being used to reason about a vast range of computational paradigms including:

* finding security violations in web and mobile applications such as JavaScript and Android.
* establishing properties of biological systems (e.g. DNA computation)
* finding serious errors in systems software (e.g. Linux kernel, device drivers, file systems)
* automatic discovery of new algorithms (e.g. concurrent data structures, distributed algorithms) and end-user programming.
* compilers for domain specific languages
* architecture-driven reasoning of concurrent software (e.g. Intel's x86, ARM, IBM's Power).

This course will provide a comprehensive introduction to modern, state-of-the-art program analysis concepts and practical frameworks including:

* Dynamic Analysis:
- concepts: memory safety, typestate, concurrency analysis
- frameworks: Valgrind, FastTrack, EventRacer

* Static Analysis:
- concepts: abstract interpretation (domains, soundness, precision, fixed points)
- frameworks: Apron, PPL

* Security Analysis:
- concepts: static + dynamic combination
- example: malware detection

* Pointer analysis:
- concepts: Andersen's, Steensgaard's analysis
- frameworks: Soot, LLVM, WALA

* Program synthesis:
- concepts: L*, version spaces, PBE, CEGIS
- frameworks: Sketch, AGS, SmartEdit, ReSynth

* Predicate abstraction:
- concepts: Graf-Saidi, Boolean programs, lazy abstraction
- frameworks: Microsoft's SLAM for C programs, Fender

* Symbolic execution:
- concepts: SMT, concolic execution
- frameworks: S2E, KLEE, Sage

* Applications of Analysis & Synthesis:
- GPU programs, security errors, device drivers, concurrent algorithms, end-user programming.

To gain a deeper understanding of how to apply these techniques in practice, the course will involve a small hands-on programming project where based on the principles introduced in class, the students will build a program analyzer for a modern programming language.
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 4 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 the semester-long project (30%) and final exam (70%).
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 2 hrs
Wed 09-11 CHN D 46 »
M. Vechev
263-2910-00 U Program Analysis 1 hrs
Wed 11-12 CHN D 46 »
M. Vechev

Restrictions

There are no additional restrictions for the registration.

Offered in

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