Program Verification

News

• There will be oral exams on 12th March and 19th March between 14:00 and 18:00. Please contact the examination office (Prüfungsamt) to schedule time and date of your exam.
• Please participate in the course evaluation. Fill the English version or the German version of the course evaluation form and submit it until 1st Feb to either Julian Jarecki, Matthias Heizmann (building 52, room 00-019), or sent the form via email to studienberatung@informatik.uni-freiburg.de.
  
• There will be no lecture on Mon 23rd January, Tue 24th January, Mon 30th January, and Tue 31st January. However there will be tutorial sessions in both weeks. Please deliver solutions of your exercise sheets until Tuesday 16:00 either directly to Julian Jarecki, to the office of Matthias Heizmann (building 52, room 00-019), or the the secretary's office of our chair (building 52, room 00-023).
  
• On Thursday 15th of December the tutorial session will not start at 16:00 c.t. but after the annual Christmas lecture of our faculty (which will take around one hour).
  
• There will be no lecture on Monday 5th December.
  
• On Tuesday 29th November there will be the talk Mathematical Challenges in the Electronics Industry by Joost Rommes in the seminar room of the third floor of building 103. We want that you are able to attend there and start with our lecture after this talk (around 16:35).
  
• There will be no lecture on Tuesday 22nd November. Please deliver solutions of your exercise sheets to Julian Jarecki, Matthias Heizmann, or the secretary's office of our chair until 16:00 on 22th November.
• Due to illness there will be no lecture on Monday 14th November.
  
• Solutions for the exercise sheets have to be submitted in the lecture on Tuesday. (Only in the second week submission on Monday was necessary since Tuesday was a holiday.
  
• The weekly tutorial sessions (Übungsgruppen) will be Thursdays 16:00-17:00 c.t. in building 101 SR 01-016.
  
• We deviate from the course catalog. Classes will be on Monday and Tuesday from 16:00-18:00. However at some dates (e.g., the week before Christmas) we will skip the lecture. If we skip the lecture, this will be announced in advance on this website. Overall we will have the same amount of lectures as any other 3+1 course. (weeks of semester * 3).
• The first exercise sheet is issued. All exercises are relevant for the lecture and the exam. However, since you have only four days to solve the exercises we decided that every point on this exercise sheet is a bonus point.
  The solutions for the first exercise sheet have to be submitted on Monday 31.10.2011 in the lecture.
  The first exercise group takes place in the second week of the lecture period, probably on Thursday 3.11.2011
  

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 behaviours.

In the lecture, 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 leads to system crash or deadlock, unexpected exceptions, and the failure of runtime checks. We can formalize such rules, for example by a finite automaton. Below a small program for which we would like to know whether it obeys the rule that 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 below (the red state is the accepting state of the automaton the automaton accepts exactly the words that correspond to a bad behaviour). Is the program correct? Today tools exist that can answer this question automatically.

Example() { 1: do{       lock();       old = new;     q = q->next; 2:    if (q != NULL){ 3:        q->data = new;        unlock();          new ++;       } 4: } while(new != old); 5:  unlock ();     return; }

Slides

Exercises

The lecture is accompanied by weekly tutorial sessions (Übungsgruppen) held by Julian Jarecki.

• Each week we will publish an exercise sheet here.
• In the following week you will submit your solution.
• We will review your solutions and grade it in a point system.
  
• You are admitted to the exam only if you obtained at least 50% of the points  for the exercises (we don't like this requirement ourselves but we have experienced too many disasters without it).
  
• In the exercise group we will discuss the solutions.
  

Exam

There will be oral exams on 12th March and 19th March between 14:00 and 18:00. Please contact the examination office (Prüfungsamt) to schedule time and date of your exam.  As said above, you may  participate in the exam only if you have obtained at least 50% of the points for the exercises.

Literature

• Almeida, J.B., Frade, M.J., Pinto, J.S., Melo de Sousa, S., Rigorous Software Development An Introduction to Program Verification, Springer 2011, ISBN 978-0-85729-017-5
• Andrey Rybalchenko: Constraint Solving for Program Verification: Theory and Practice by Example. CAV 2010:57-71