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

Program Verification (Lecture)

Course Type Lecture
 Instructors Matthias Heizmann, Dominik Klumpp, Andreas Podelski
Lecture Monday 16:15 - 18:00
Wednesday 16:15 - 18:00
Online a the BBB virtual classrom
Exercise Closely integrated to the lecture
Language English
Exam tba
 Course Catalog Program Verification (Lecture)
Program Verification (Exercise)

News

2021-04-15: The course website is now online. If you want to get an impression of this courses content, you can watch one of the three videos of last year's lecture.

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.

E-Learning

The course will be organized online in the Ilias system.The main course material are slides and exercises. Additionally we will have interactive sessions via BigBlueButton, which is integrated in Ilias. The interactive sessions are NOT recorded.

The slide set consists of three kinds of slides. First, there are slides that I would show in a presentation. Some of these slides are accompanied by additional slides (the slides with violet text) that contain the information that I would say while giving the presentation. Furthermore there are slides that look like titlepages, have blue background and tell you the range of slides that is discussed in the next virtual classroom.

The slides are very similar to a lecture script and the idea is that you read the slides before the next interactive sessions. Your efforts to understand the slides will be supported by exercises that you hand in before the next interactive sessions. In the interactive sessions we will go very quickly through the slides and discuss only your questions. Furthermore, we will discuss your solutions for the exercises.

We are very happy to improve the course material. If you have questions and you think something should be explained in more detail then please let us know.

Slides

The lecture slides are the main course material. Starting from Section 2 the slides are annotated with additional information and can be seen as a kind of lecture script.

The slides will be updated frequently. We will not only append new content but depending on the questions in interactive sessions we will also insert slides with additional information.

 

Exercises

Exercise sheets will be uploaded and submitted (electronically) in Ilias.
  • An exercise sheet will be uploaded every Wednesday evening and should be submitted (in Ilias) by the following Monday.
  • Furthermore, we will have short exercise sheets on Monday in preparation for the next lecture, to be submitted by Wednesday.
 
 
 
Submission deadlineExercise sheet
Wednesday 21th April 16:00

Exercise sheet 00 (see Ilias)

Monday 26th April 10:00 Exercise sheet 01
Wednesday 28th April 16:00 Exercise sheet 02
Monday 3rd May 10:00 Exercise sheet 03
Wednesday 5th May 16:00 Exercise sheet 04
Monday 10th May 10:00 Exercise sheet 05
Wednesday 12th May 16:00 Exercise sheet 06
Monday 17th May 10:00 Exercise sheet 07
Wednesday 19th May 16:00 Exercise sheet 08
Monday 31rd May 10:00 Exercise sheet 09
Wednesday 2nd June 16:00 Exercise sheet 10
Monday 7th June 10:00 Exercise sheet 11
Wednesday 9th June 16:00 Exercise sheet 12
 Monday 14th June 10:00 Exercise sheet 13
 Wednesday 16th June 16:00 Exercise sheet 14
Monday 21st June 10:00 Exercise sheet 15
  Wednesday 23rd June 16:00 Exercise sheet 16
 Monday 28th June 10:00 Exercise sheet 17
   Wednesday 30th June 16:00 Exercise sheet 18
  Monday 5th July 10:00 Exercise sheet 19
   Wednesday 7th July 16:00 Exercise sheet 20
   Monday 12th July 10:00 Exercise sheet 21
    Wednesday 14th July 16:00 Exercise sheet 22
    Monday 19th July 10:00 Exercise sheet 23
     Wednesday 21th July 16:00 Exercise sheet 24

 

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 presented an exercise in an interactive session.

Literature