Program Verification (Lecture)

News

• 2026-06-02: exam conditions announced
• 2026-04-21: ILIAS course published
• 2026-04-20: the exercise sessions start on April 28
• 2026-03-27: course website online

Motivation

Contents

Although this lecture involves practical tools, it is primarily theoretical in nature, focusing on the fundamental concepts of program verification.

As a basis, we will use mathematical logic (if you dislike mathematical logic, this lecture may not be for you). We will often reduce problems to the satisfiability problem of logical formulas. For example, 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. For example, 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

Each Monday, there will be an in-presence lecture.

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

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). There will be time slots both near the beginning of the examination period (10th - 12th August) and near the end (14th - 16th September).

Note that the exam registration period runs from 1st June 2026 to 12th July 2026 (see here). You must register for the exam via HisInOne within this time frame in order to take the exam (even if no date is shown in HisInOne).

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