Program Analysis (Winter Semester 2020/21)
Quick Facts
| Lecturer | Prof. Dr. Michael Pradel |
| Teaching assistants | Aryaz Eghbali, Luca Di Grazia, Daniel Lehmann, Jibesh Patra, Moiz Rauf |
| Course type | Lecture + Exercises |
| Language | English |
| Ilias | Ilias course with forum and quizzes |
| Place | Virtual |
Content
This course introduces the principles and practice of automatically analyzing large software systems. The course provides an overview of program analysis and then covers three topics in more detail: Static analysis, which analyzes the source code of a program, dynamic analysis, which reasons about the runtime behavior of a program, and test generation, which creates inputs to run programs. In addition to lectures, students will deepen their understanding through a practical course project (implement a program analysis based on an existing framework) and homework assignments. Besides academic achievements, the course will help students to improve their programming skills by learning about common sources of mistakes and about techniques to find them.
Schedule
This is a preliminary schedule and may be subject to change. "L" stands for lecture, "P" stands for project, and "E" stands for exercise. Lectures will be distributed via YouTube and have a recommended time window to watch them (but you can watch them any time). Events with a precise date happen on that date. Events printed in italics happen synchronously via Webex and will not be recorded, i.e., you should plan to attend them at the given time. Events printed in bold are deadlines (strict).
| Date | Topic | Material |
|---|---|---|
| Nov 2 to Nov 6, 2020 | L: Introduction |
Part 1 (Motivation): Lecture, Slides Part 2 (Organization): Lecture, Slides Part 3 (Basics): Lecture, Slides |
| Nov 9 to Nov 13, 2020 | L: Operational semantics |
Part 1 (Preliminaries): Lecture, Slides Part 2 (Syntax of SIMP): Lecture, Slides Part 3 (Abstract machine): Lecture, Slides Part 4 (Small-step semantics): Lecture, Slides Part 5 (Big-step semantics): Lecture, Slides Fernandez' book Pitts' lecture notes |
| Nov 13, 2020 | E: Exercise 1 (operational semantics) published | Exercise, Solution |
| Nov 16 to Nov 27, 2020 | L: Data flow analysis |
Part 1 (Available expressions): Lecture, Slides Part 2 (Basic principles): Lecture, Slides Part 3 (More examples): Lecture, Slides Part 4 (Solving): Lecture, Slides Part 5 (Inter-procedural): Lecture, Slides Part 6 (Sensitivities): Lecture, Slides Chapter 2 of Principles of Program Analysis |
| Nov 20, 2020 | E: Exercise 1 due | |
| Nov 23, 2020, 11:30-13:00 | E: Discussion of exercise 1 | |
| Nov 27, 2020 | P: Project description published |
Project description Code Template for final report |
| Nov 30 to Dec 4, 2020 | L: Call graph analysis |
Part 1 (Introduction): Lecture, Slides Part 2 (CHA, RTA): Lecture, Slides Part 3 (VTA, DTA): Lecture, Slides Part 4 (Spark): Lecture, Slides Paper by Lhoták and Hendren Soot framework |
| Dec 7 to Dec 11, 2020 | L: Random testing and fuzzing |
Part 1 (Introduction): Lecture, Slides Part 2 (Feedback-directed random fuzzing, Randoop): Lecture, Slides Part 3 (Greybox fuzzing, AFL): Lecture, Slides Randoop: Tool, Paper by Pacheco et al. AFL: Tool, Technical documentation |
| Dec 14, 2020 (individual time slots) | P: Progress meeting 1 | |
| Dec 14 to Dec 22, 2020 | L: Symbolic and concolic execution |
Part 1 (Symbolic): Lecture, Slides Part 2 (Challenges): Lecture, Slides Part 3 (Concolic): Lecture, Slides Part 4 (Applications): Lecture, Slides Papers on DART, KLEE, and SAGE |
| Dec 22, 2020 | E: Exercise 2 (symbolic and concolic execution) published | Exercise, Solution |
| Jan 11 to Jan 15, 2021 | L: Information flow analysis |
Part 1 (Introduction): Lecture, Slides Part 2 (Policies): Lecture, Slides Part 3 (Analysis): Lecture, Slides Papers by Denning and by Clause et al. |
| Jan 11, 2021 (individual time slots) | P: Progress meeting 2 | |
| Jan 15, 2021 | E: Exercise 2 due | |
| Jan 18, 2021, 11:30-13:00 | E: Discussion of exercise 2 | |
| Jan 18 to Jan 22, 2021 | L: Slicing |
Part 1 (Introduction): Lecture, Slides Part 2 (Static slicing): Lecture, Slides Part 3 (Thin slicing): Lecture, Slides Part 4 (Dynamic slicing): Lecture, Slides Papers by Weiser, Sridharan et al., Agrawal et al., and Tip |
| Jan 22, 2021 | E: Exercise 3 (Information flow and slicing) published | Exercise, Solution |
| Jan 25, 2021 (individual time slots) | P: Progress meeting 3 | |
| Jan 25 to Jan 29, 2021 | L: Path profiling |
Part 1 (Introduction): Lecture, Slides Part 2 (Algorithm): Lecture, Slides Part 3 (Generalization): Lecture, Slides Paper by Ball and Larus |
| Jan 29, 2021 | E: Exercise 3 due | |
| Feb 1, 2021, 11:30-13:00 | E: Discussion of exercise 3 | |
| Feb 1 to Feb 12, 2021 | L: Analysis of concurrent programs |
Part 1 (Introduction): Lecture, Slides Part 2 (Data Races): Lecture, Slides Part 3 (Thread Safety): Lecture, Slides Part 4 (Interleavings): Lecture, Slides Papers on Eraser, ConTeGe, and CHESS |
| Feb 12, 2021 | P: Project due | |
| Feb 15 to Feb 19, 2021 | Presentation of course projects | |
| Mar 3, 2021 | Final exam | Questions Solutions |
Course Project
The course project is about implementing a static taint analysis for JavaScript based on the general data flow analysis framework. More details will be published during the semester.
