« April 2017 »
April
MoTuWeThFrSaSu
12
3456789
10111213141516
17181920212223
24252627282930
Uni-Logo
You are here: Home Teaching Summer Term 2017 Program Verification (Lecture)
Document Actions

Program Verification (Lecture)

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

News

  • To get an impression of what this course is about, students may want to have a look at a previous course.

Contents

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.

 rules-directx.pngrules-unix.pngrules-windows.pngrules-linux.png

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

Slides are found here.

 

 

Exercises

In this lecture we aim for active discussions in the exercise group. We organize the exercise group in a new way, where each exercise will be presented by 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 Doodle in which each student should rank each exercises according to his or her willingness to present the exercise in the next exercise group.
  • Until Friday 19: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 7: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.

Exam

There will be an oral exam during the examination period. Prerequisite for admission to the exam is an active participation in the exercises.

Literature

Personal tools