Program Verification (Lecture)

Motivation

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

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;
}

Slides

Lecture slides

Slides (June 19) Presentation Mode

Exercises

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

• 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
• 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