Program Verification (Lecture)

Course Type	Lecture
Instructors	Dominik Klumpp, Frank Schüssele, Lena Funk, Prof. Andreas Podelski
Lecture	Monday 16:15 - 18:00, room SR 01-009/13, building 101 Wednesday 14:15 - 16:00, room HS 00-026, building 101
Exercise	Closely integrated to the lecture
Language	English
Exam	oral exam; see details below
Course Catalog	Program Verification (Lecture)

News

2024-05-27: exam conditions announced
2024-04-02: link to ILIAS course added
2024-04-02: course website online

Motivation

Did you ever write a computer 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:

We can write tests. We check for a given input if the program produces the expected output
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.

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

void foo(unsigned int x, unsigned int y) {
    while (x+y <=42) {
        if (y >= 100) {
            x = 2 * x - y;
            //@ assert (x+y >= 100);
        }
        y++
    }
}

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.

int main() {
    unsigned char pos = getInitialPosition();
    int arr[256];
    while(1) {
        arr[pos] = getNextValue();
        arr[pos + 1] = getNextValue();
        pos += 2;
    }
    return 0;
}

Lecture

There will be two in-presence lectures each week. Exercise sessions (see below) are integrated into the lectures.

The main course material are slides and exercises. The lecture slides are very similar to a lecture script, and consist of two kinds of slides. First, there are slides that I would show in a presentation. Second, some of these slides are accompanied by additional slides (the slides with violet text) with more detailed information. We will update the slides throughout the semester.

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.

Exercises

We will upload two exercise sheets every week:

Every Monday evening, we will upload a short exercise sheet. The short exercise sheet is meant to help prepare the lecture on Wednesday, and should be submitted before the lecture (Wednesday, 14:00).
Every Wednesday evening, we will upload a longer exercise sheet. This exercise sheet should be submitted by the following Monday before the lecture (Monday, 16:00).

You can submit your solutions to the exercises electronically via ILIAS. Your submissions will be marked and you will receive individual feedback. Additionally, we will discuss the solutions to the exercises at the beginning of each lecture.

You are allowed (and we encourage you) to discuss the exercises and possible approaches to solutions with your fellow students. However, please write down and submit your solution by yourself.

To pass the "Studienleistung" for this lecture, you must obtain at least 50% of the exercise points (summed up over all exercise sheets), and you must present at least one exercise in the exercise sessions. The idea is that you train yourself to write down things in a formally correct way, and practice speaking about the concepts of the lecture. Your solutions to the exercises will help us to evaluate your knowledge and adapt the lecture accordingly.

Programming Exercises

In addition to the theoretical exercises, we offer bonus exercises in which you can implement some of the verification techniques discussed in the lecture.

We provide a basic framework written in Python3 (e.g. parsing using ANTLR4, and SMT support using PySMT). Additional exercise sheets describe the parts of the code you have to implement in order to be able to run an analysis technique on programs written in the simple programming language introduced in the lecture.

All programming exercises are bonus exercises. Any bonus points collected here count towards the exercise points required for the "Studienleistung" (see above).

Exam

There will be an oral exam at the end of the semester. The exam will consist of a 25 min conversation in which we ask you about the content of the lecture. No notes or additional materials will be permitted. We will provide pen and paper in case they are needed to help with an explanation or example.

We will set up a booking pool for individual exam time slots via ILIAS. These will be made available after exam registration ends (middle of July). We are planning to offer time slots both near the beginning of the examination period (7th - 9th August) and near the end (11th - 13th September).

Note that the exam registration period runs from 27th May 2024 to 7th July 2024 (see here). You must register for the exam via HisInOne within this time frame in order to take the exam.

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
Apt, Boer, Olderog, Verification of Sequential and Concurrent Programs, Springer 2009, ISBN 978-1-84882-744-8
Clarke, Henzinger, Veith, Bloem, Handbook of Model Checking, Springer, 2018, ISBN 978-3-319-10574-1
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model Checking for People Who Love Automata. CAV 2013