Navigation
Home > Teaching > Static Program Analysis

Advanced Course Static Program Analysis

Summer term 2011

Prof. Dr. Reinhard Wilhelm, Jörg Herter, M.Sc.

News

  • There exists now a mailing list for all participants of the course: spa11@gigasun.cs.uni-saarland.de
    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

Lecture Slides

General Information

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

Requirements

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.

Content

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.

Projects

Exercises

Tutorial Group A (Thu, 10-12, SR015)Tutorial Group B (Fri, 10-12, SR107)
Kaiser, Jonas
Nalbach, Oliver
May, Eva
Schneider, Sigurd
Hahn, Sebastian
Boesche, Klaas
Xu, Haiyang
Jacobs, Michael
Lautemann, Nadine
Haupenthal, Florian
Schaub, Thomas
Teris, Liviu
Köhl, Andreas
Köhl, Christian
 Legrum, Andreas
Knopp, Nikolai
Schommer, Bernhard
Höschele, Matthias
Zickenrott, Sascha
Goncharova, Anastasiya
Weigel, Martin
Tebbi, Tobias
Dörr, Barbara
Graf-Brill, Alexander
Ebert, Caroline
Harz, Maximilian
Gökkaya, Hilmi
Chernev, Iskren
Farooq, Imran
Ellinghaus, Tobias
Ansari, Farzaneh

Literature