« May 2017 »
You are here: Home Teaching Summer Term 2017 Program Verification (Lecture)
Document Actions

Program Verification (Lecture)

Course Type
 Instructors Prof. Dr. Andreas Podelski, Dr. Matthias Heizmann, Christian Schilling
Tuesday 17:00-18:00 c.t. in building 101-00-036
Wednesday 16:00-18:00 c.t. in building 101-00-036
Tuesday 16:00-17:00 s.t. in building 101-00-036
Language English
 Course Catalog
Program Verification (Lecture)
Program Verification (Exercise)


  • May 25: Exercise Sheet 5 has been finalized.
  • May 11: We removed an exercise from Exercise Sheet 3 because the respective theory was not discussed in the lecture.
  • May 11: We moved the deadline for the exercise ranking from Friday 7 p.m. to Sunday 8 p.m. Furthermore, the assignment results will be made available on Monday 9 a.m. (instead of 7 a.m.).
  • May 5: We added the exercise ranking form for Exercise Sheet 2 with some delay.
  • May 3: We clarified the examination admission requirement.
  • Apr 29: The ranking form for Exercise Sheet 1 has been added.
  • Apr 28: This week the deadline for submitting the exercise rankings was extended to Sunday.


Often computers are used in embedded, networked, safety critical applications. The cost of failure is high.

In this lecture we introduce the basis of automatic tools for ensuring that a system does not have bad behaviors.

We start with a short introduction to propositional logic and first-order reasoning.

We then go on to establish a setting for the verification of programs whose correctness is specified by a kind of program comments. In this setting, the correctness of the program is reduced to the validity of logical formulas. The validity is proven automatically by a new generation of powerful reasoning engines.

Finally, we connect verification with static analysis methods that have been developed originally in compiler optimization and which are formalized by Patrick and Radhia Cousot's framework of abstract interpretation.


Example of a verification problem.  Technical documentation, for example of device driver programs for Windows and Linux operating systems, contains rules that specify the order of certain operations and file accesses. A violation of such a rule can lead to system crashes, deadlocks, unexpected exceptions, or the failure of runtime checks. We can formalize such rules, for example by a finite automaton. Below is a small program for which we would like to know whether it obeys the rule "calls to lock and unlock must alternate" (an attempt to re-acquire an acquired lock or release a released lock will cause a deadlock). The rule can be formalized by the automaton shown next to the program (the red state is the accepting state of the automaton, i.e., the automaton accepts exactly the words that correspond to a bad behavior). Is the program correct? Today tools exist that can answer this question automatically.



Slides are found here.



If you do not want to use the Google form, you can alternatively send you rankings via email to Matthias Heizmann.

In order to incite active discussions in the exercise group, we will organize the exercise group in a new way.  The main novelty lies in the fact that, for each exercise, the solution will be presented by a team of two students.

  • Solutions of exercises will be neither corrected nor graded.
  • You can only achieve exercise points for presenting solutions in the exercise group.
  • Each Wednesday, we will upload an exercise sheet on this website.
  • Furthermore, there will be a link to a form in which each student should rank each exercises according to his or her willingness to present the exercise in the next exercise group.
  • Until Sunday 20:00 everyone has to submit his or her rankings.
  • Over the weekend we will assign (randomly if necessary) two students to each exercise.
  • The assignment results will be made available before Monday 9:00.
  • The two students that are assigned to an exercise have to coordinate and present a solution together in the exercise group on Tuesday.
  • It is not necessary to present a perfect solution, but we expect that you are able to present an approach for finding a solution that we can discuss together.
  • We expect that everyone participates actively in the discussion of the solution.


There will be an oral exam during the examination period. Prerequisite for admission to the exam is an active participation in the exercises. A sufficient criterion for an active participation is that you received 8 exercise points.


Personal tools