Overview
The last decade has seen an explosion in techniques for automated program analysis. Modern program analysis techniques are widely applicable and have thus enabled a vast range of interesting applications: from ensuring correctness of complex parallel algorithms to finding security violations in mobile applications, to reasoning about biological DNA systems, and even to code synthesis.
This course will cover the core principles behind these automated techniques including static and dynamic program analysis, symbolic execution, predicate abstraction, pointer analysis, combinations with machine learning techniques, and others. We will also cover practical analysis frameworks such as Soot, Wala and LLVM.
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 reasoning engine for a modern programming language.