Advanced Course Program Analysis and Transformation

Summer term 2007

Prof. Dr. R. Wilhelm, S. Altmeyer


News

30.5.2007
Fifth exercise sheet online.

15.5.2007
Third exercise sheet online.

9.5.2007
Second exercise sheet online.

3.5.2007
The dates for the lecture are now fixed:
Lecture: Tuesday 11-13 (room 401, E1.3)
Tutorial group: Wednesday 9-11 (room 401, E1.3)
The last friday lecture (4.5.2007) also takes place in room 401.

3.5.2007
The dates for the lecture are now fixed:
Lecture: Tuesday 11-13 (room 401, E1.3)
Tutorial group: Wednesday 9-11 (room 401, E1.3)
The last friday lecture (4.5.2007) also takes place in room 401.

23.4.2007
After this week, the lecture will be rescheduled; please e-mail me (altmeyer(at)cs(dot)uni-saarland(dot)de) your preferences. (But, this week, the lecture will be on friday 9-11 once again.)
Please read the first 20 pages from the script. You can get these pages in my office (Room 402, Building E1 3).

General Information

Type: advanced course (6 credit points)
Place: room 401, E1.3
Date: Tu. 11-13
Exam: 20.7.2007
Time and place for the exercise still have to be fixed
For further information send mail to: altmeyer(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 the exam and on the projects.

Content

Program Analysis is a technique to statically determine dynamic properties of programs. These dynamic 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 from them. Thus, they will in general be incomplete, i.e., not all satisfied properties can be found out to hold.

Program analysis has been established as a technique used in optimizing compilers, where it was used to gather information about the program enabling optimizing 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 arrays index will never be out of bounds, the store operation into a buffer will never overflow the buffer.

A surprising and successful application of program analysis in the Compiler Design Lab at Saarland University is the determination of upper bounds on the execution times of programs. These upper bounds are needed for hard real-time systems as they are frequent in the automotive and the avionics domain. Program analysis is used here to derive safety properties such as, at this program point, instruction fetch will never cause a cache miss.

The same group is cooperating in the development of another program-analysis technique, namely the so-called Shape Analysis. This technique was originally developed to determine shapes of heap-allocated data structures. Meanwhile, it has been applied to verify partial correctness of programs and synchronization properties of multi-threaded programs.

Literature