You are here: Home Teaching Summer Term 2019 Program Verification (Lecture)

Program Verification (Lecture)

Course Type
Lecture
 Instructors Dr. Matthias Heizmann, Tanja Schindler, Dominik Klumpp
Lecture
Monday 16:00-18:00 c.t. in building 101 room 01-009/013
Wednesday 16:00-18:00 c.t. in building 101 room 01-009/013
Exercise
Closely integrated to the lecture
Language English
Exam
There will be an exam.
 Course Catalog
Program Verification (Lecture)
Program Verification (Exercise)

Motivation

Did you ever write compute program that did not work correctly? Perhaps surprisingly for outsiders the response of every programmer will be "yes" because especially during the development of software, faulty programs are rather the rule than the exception.

How do we deal with the problem that we often have errors in our code? There are two typical approaches:

  1. We can write tests. We check for a given input if the program produces the expected output
  2. We can analyze our code very carefully.

Did you ever have a bug in you code even if you analyzed it very carefully and did some tests? Even to this question, the answer "yes" is no surprise, since tests cannot capture all behaviors of the program and an analysis of code is tedious and error-prone. From our everyday experience with electronic devices, we know that not only computer science students but also professional programmers regularly fail to write correct code. The fact that there is a long list of faulty software systems that were expensive or safety-critical hints that the problem is not just the sloppiness of programmers but that there is a need for new approaches that improve the reliability of software.

In this lecture we will learn an approach that is called software verification. First, we will formally state properties like e.g., if the program reaches line 42 then the variable x is positive, or if the input is different from 23 then there will be no overflow. We will then learn how to write mathematical proofs that show that a given program satisfies a given property.

Unfortunately, it can be tedious and difficult to find such a mathematical proof and humans also tend to make mistakes while giving mathematical proofs. Hence, we would like to let computers do this task.

In this lecture we will see algorithms that enable computers to find bugs in computer programs, or to find proofs that show the absence of bugs.

 

Contents

Although we will use tools this is a rather theoretical lecture in which we will learn the basic concepts of program verification.

We will often reduce problems to the satisfiability problem of logical formulas. (So if you do not like mathematical logic, you probably do not want to take this lecture.) E.g, a satisfying assignment for the following formula will show us how the assert statement in the depicted program can be violated.

  x_0 >= 0 /\ y_0 >=0 /\ x_0<=4294967296 /\ y_0<=4294967296 /\ x_0 + y_0 <= 42 /\ y_0 >= 100 /\ x_1 = (2*x_0-y_0)%4294967296 /\ x+y < 100

 

In order to get familiar with logical reasoning, the course will start with an introduction to propositional logic and first-order logic. We will then formally introduce the Hoare calculus which will allow us to state the correctness of a program and to give a mathematical proof that the program is correct.

Throughout this lecture, we will use tool like the Z3 SMT solver or the Ultimate Automizer software verifier in order to see the effect of our algorithms on practical examples. E.g., if we want to find out if the following C program is correct, we can ask Ultimate Automizer.

 

 

 

Slides

Lecture slides

Slides (June 19) Presentation Mode

 

Exercises

Submission deadline
Exercise sheet
Monday 29th April 10:00

Exercise sheet 01

Monday 6th May 10:00

Exercise sheet 02

Wednesday 8th May 16:15
Exercise sheet 03
Monday 13th May 10:00

Exercise sheet 04

Wednesday 15th May 16:15  Exercise sheet 05
Monday 20th May 10:00

Exercise sheet 06

Wednesday 22nd May 16:15 Exercise sheet 07
Monday 27th May 10:00

Exercise sheet 08

Wednesday 29th May 16:15 Exercise sheet 09
Monday 3rd June 10:00

Exercise sheet 10

Wednesday 5th June 16:15 Exercise sheet 11
Monday 17th June 10:00

Exercise sheet 12  (corrected version)

Additional material for exercise 5

Wednesday 19th June 16:15 There will be no exercise sheet 13
Monday 24th June 10:00

Exercise sheet 14

Wednesday 26th June 16:15 Exercise sheet 15
Monday 1st July 10:00

Exercise sheet 16

Wednesday 3rd June 16:15 Exercise sheet 17
 Monday 8th July 10:00

Exercise sheet 18

Wednesday 10th June 16:15
 Exercise sheet 19
  Monday 15th July 10:00

Exercise sheet 20

 Wednesday 17th June 16:15   Exercise sheet 21
   Monday 22th July 10:00

Exercise sheet 22

 Wednesday 24th June 16:15 Exercise sheet 23

Please submit your solutions via email to Dominik Klumpp, or via the top right post box located in the ground floor of building 051. Solutions for the (short) exercise sheets that have to be submitted on Wednesdays can also be handed in at the beginning of the lecture.

Exam

There will be an 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 in the exercises is that you achieved 50% of the points that can be obtained for exercise sheets and you presented one exercise in the class.

Literature