Program Verification (Lecture)

News

• April 15: In the first week there will be lectures on Monday and Wednesday
  

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.

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.

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

The lecture slides will be made available here.

• Trace Abstraction
• AbtractRefineLoop
  
• Abstraction Refinement
  
• Predicate Abstraction
  
• Reachability Analysis (continued)
  
• Strongest Postcondition and Reachability Analysis
  
• Guarded Commands
  
• Generation of Verification Conditions
  
• Hoare logic
  
• First-order logic
  
• Propositional logic
• Abstract interpretation
  
• Overview
  

Exercises

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

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.
• Until Thursday 22:00 everyone has to write an email to Matthias and state his or her interest in presenting the solutions in the exercise group. Please rate in your email each exercise between 1 (I would prefer that someone else presents this exercise) and 10 (I would like to present this exercise very much).
  
• We will assign (randomly if necessary) two students to each exercise.
• The assignment results will be made available on Friday morning.
• The two students that are assigned to an exercise have to coordinate and present a solution together in the exercise group on Monday.
• 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 exam during the examination period. Prerequisite for admission to the exam is an active participation in 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
• Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model Checking for People Who Love Automata. CAV 2013

• Traces, interpolants, and automata : Ultimate Automizer’s approach to software verification
  Talk given at the EPIT Spring School 2018