263-2910-00L Program Analysis
Semester | Autumn Semester 2013 |
Lecturers | M. Vechev |
Periodicity | yearly recurring course |
Language of instruction | English |
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: Link |
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. |