Advanced Course Static Program Analysis
Summer term 2011
- There exists now a mailing list for all participants of the course: email@example.com
If you participate in the course, please make sure you are on that list.
- We started a Doodle poll to find suitable time slots for the tutorial sessions. Please 'vote' until Sunday, 17th. You find the poll here
- 11/04/13: Introduction and Principles of Program Analysis (by Flemming Nielson & Hanne Riis Nielson & Chris Hankin).
- 11/04/27: Available Assignments, Lattices, and Fixpoint Iteration (Annotated lecture slides): [Part A] [Part B]
- 11/05/04: Live Variables and 'Superfluous Moves' (annotated version) and Constant Propagation (annotated version)
- 11/05/11: Interval Analysis
- 11/05/18: Fixed-Point Algorithms
- 11/05/25: Alias Analysis
- 11/06/08: Shape Analysis and Partial Redundancy Elimination
- 11/06/22: Loop Invariant Code and Elimination of Partially Dead Code
- 11/06/29: Interprocedural Analysis
- 11/07/13: Introduction to Timing Analysis, Cache Analysis, and Pipeline Predictability
Type: advanced course (6 credit points)
Place: lecture hall 001, E1.3 (lecture); 015, E1.3 (tutorial group A), 107, E1.3 (tutorial group B)
Time: Wed. 10 - 12 (lecture); Thu. 10 - 12 (tutorial group A), Fri. 10 - 12 (tutorial group B)
Exam: 03.08.2011, 10.00 - 12.00 hrs; 003, E1.3
Re-Exam: 21.09.2011, 10.00 - 12.00 hrs; 003, E1.3
For further information, you can contact Jörg via jherter(at)cs(dot)uni-saarland(dot)de
To pass the lecture, you have to work on some projects and you have to pass the exam at the end of the term. The grade will be based on both, the exam and the projects. To be admitted to the exam, you need at least 50% of the points from the exercise sheets.
Program Analysis is a technique to statically determine properties of programs.
These properties are in principle undecidable.
Therefore, only approximate answers can be given.
These answers have to be safe, that is, no false conclusions should be drawn.
Hence, they will in general be incomplete, i.e., not all satisfied program properties can be found out to hold.
Program analysis has been established as a technique used in compilers, where it is used to gather information about the program in order to enable optimizing program transformations. In the last years, it has found many applications in software validation. Program analysis verifies invariants at program points. These invariants can be used to derive safety properties about the program such as "the division at this program point will never divide by 0", "the array's index will never be out of bounds", "the store operation into a buffer will never overflow the buffer", and so on.
A surprising and successful application of program analysis in the Compiler Design Lab at Saarland University is the determination of safe upper bounds on the execution times of programs. These upper bounds are needed for hard real-time systems frequently occuring in the automotive and avionics domain. There, program analysis is used to derive safety properties such as "at this program point, an instruction fetch will never cause a cache miss".
The same group is cooperating in the development of another program-analysis technique, the so-called Shape Analysis. This technique was originally developed to determine shapes of heap-allocated data structures. Today, it has additionally been applied to successfully verify partial correctness of programs and synchronization properties of multi-threaded programs.
- Exercise Sheet 9 (updated 07/13 22:46)
- Exercise Sheet 8
- Exercise Sheet 7
- Exercise Sheet 6
- Exercise Sheet 5
- Exercise Sheet 4
- Exercise Sheet 3
- Exercise Sheet 2
- Exercise Sheet 1
|Tutorial Group A (Thu, 10-12, SR015)||Tutorial Group B (Fri, 10-12, SR107)|
Helmut Seidl, Reinhard Wilhelm, Sebastian Hack.
Übersetzerbau 3: Analyse und Transformation
Springer, Berlin; Auflage: 1., st Edition. (Dezember 2009)
Flemming Nielson, Hanne Riis Nielson, Chris Hankin:
Principles of Program Analysis.
Springer, (450 pages, ISBN 3-540-65410-0), 1999
Patrick Cousot and Radhia Cousot.
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.
In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238--252, Los Angeles, California, 1977. ACM Press, New York.
Patrick Cousot and Radhia Cousot.
Systematic Design of Program Analysis Frameworks.
In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 269--282, San Antonio, Texas, 1979. ACM Press, New York.
- Reinhard Wilhelm, Dieter Maurer.
Übersetzerbau: Theorie, Konstruktion, Generierung
Springer, 1997 ISBN 3-540-61692-6