Static Program Analysis
Advanced CoursePeople
Jan Reineke, Christian Hammer, Sebastian HackGeneral Information
This course qualifies as an advanced course in the Saarland University CS program.
You have to be in the university subnet to register for the mailing list.
We will have a Q&A session for the exam in the tutorial slot on 2015-01-06 12:00 in E1.3 HS III.
The projects will be presented on 2015-01-16 14:00 in E1.3 Room 401.
Lecture
- Type: advanced lecture (9 credit points)
- Place: lecture hall II (HS II), building E1 3
- Time: Mondays 10-12 (c.t.), Wednesdays 10-12 (c.t.)
- First lecture: Wednesday, October 22
We will have lectures until Christmas. The second part of the course is a project in which you implement a program analysis.
Slides
- 2014-10-22: Introduction
- 2014-10-27: Lattices (Revision 2)
- 2014-10-29: Foundations I
- 2014-11-03: Foundations II
- 2014-11-05: Foundations III
- 2014-11-10: Static Analysis using Polyhedra
- We did not cover section 3.4 of the paper.
- Schrijver's book is an excellent reference for polyhedra in general.
Background on the different representations of polyhedra (frame, inequations) can be found in chapter 7 and 8.
Fourier-Motzkin Elimination as we presented it in the lecture is described in chapter 12, page 155
- 2014-11-13: Reaching Definitions, Interprocedural Analysis
- 2014-11-17: Interprocedural Analysis (Updated), Program Dependence Graph
- 2014-11-19: SSA
- Background reading: Cytron et al. Efficiently Computing Static Single Assignment Form ...
- 2014-11-24: Slicing
- 2014-11-26: Cache Analysis
- 2014-12-01: Cache Persistence Analysis, Further Reading: Cache persistence analysis: Theory and practice (available for download within university network)
- 2014-12-03: Research paper: Alias et al.: Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
- 2014-12-08: Research paper: Gulwani et al.: Synthesis of Loop-Free Programs
- 2014-12-10: Research paper: Reps, Sagiv, Yorsh: Symbolic Implementation of the Best Transformer, Python implementation (requires Python 3.4 and Z3)
- 2014-12-15: Points-To Analysis
Background Reading
- Nielson, Nielson, Hankin: Principles of Program Analysis
- Seidl, Wilhelm, Hack: Compiler Design: Analysis and Transformation
- Cousot: Course on Abstract Interpretation at MIT
Exercises
- Place: lecture hall III (HS 3), building E1 3
- Time: Tuesdays 12-14 (c.t.)
We will hand out (at least) 6 exercise sheets.
- Exercise Sheet 1
- Exercise Sheet 2
- Exercise Sheet 3 (due 2014-11-17)
- Exercise Sheet 4 (due 2014-11-24)
- Exercise Sheet 5 (due 2014-12-01)
- Exercise Sheet 6 (due 2014-12-08)
Exams
- 2015-01-12 10-12 HS II
- 2015-03-23 10-12 HS II
You need 50% of the points of 6 exercise sheets to be admitted to the exam.
The final Grades are now available.
Projects
We will present a list of projects after the exam on 2015-01-16. During the project phase all participants of the course will meet on a weekly basis to discuss their progress.