Verification and Testing (WS 2023/24)

Course Number 705040 | Wintersemester 2023/24


In this course, we teach various advanced methods to test and verify software and hardware. Instead of classical unit tests, we present techniques for automatic detection of bugs with little user-effort and methods to prove the correctness of a program independent of concrete input values.

The lecture starts with dynamic methods to detect and locate potential bugs related to concurrency or invalid memory accesses. Those bugs are hard to find with unit tests because they seem to show up randomly and are hard to reproduce. In the following lectures, we move on to static methods. Within these chapters, we show you how to prove the correctness of a program formally. Finally, the lecture ends with a session where we present current research topics to you. If you are interested in a master project, thesis, or internship on one of these projects, don't hesitate to contact us!

The content of this lecture includes:

  • Eraser algorithm to detect race conditions
  • Locktree algorithms to identify potential deadlocks
  • How Valgrind finds invalid memory accesses
  • Static Analysis
  • Symbolic Encoding, Bounded Model Checking, and Concolic Execution
  • Hoare Logic
  • Boolean Model Checking with the SLAM algorithm


DATE TOPIC Papers Slides
05.10.2023 Intro vt01-intro
12.10.2023 Eraser & Locktree [1] [2] vt02-concurrency
19.10.2023 Memory Debuggers vt03 - valgrind
09.11.2023 Symbolic Methods vt04 - SymbolicVerification
16.11.2023 Hoare Logic I [3] vt05-hoare-logic
23.11.2023 Hoare Logic II vt06-hoare-logic-2
30.11.2023 SLAM I vt081-SLAM-motivation-and-example.pdf
07.12.2023 SLAM II vt082 - SLAM - abstraction
14.12.2023 SLAM III vt083-SLAM-discovering-predicates vt084-SLAM-Boolean-Model-Checking
11.01.2024 Java Path Finder vt07 - jpf
18.01.2024 Current Research Topics & Question Hour


[1] Eraser: S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, T. Anderson, Eraser:A Dynamic Race Detector for Multithreaded Programs, ACM Transactions on Computer Systems Volume 15 Issue 4, November 1997. [2] Lock Tree & Java Path Finder: W. Visser, K. Havelund, G. Brat, S. Park and F. Lerda, Model Checking Programs, International Journal on Automated Software Engineering 10(2), April 2003. Extended journal version of paper presented at the ASE'00 conference. [3] Hoare Logic: Hoare-Logic course .


Z3 Tutorial



Assignment Handout Question Hour Deadline
A1 Locktree 12.10.2023 25.10.2023 17:00 10.11.2023 23:59 (extended)
A2 Hoare 16.11.2023 30.11.2023 17:30 14.12.2023 23:59
A3 SLAM 14.12.2023 11.1.2024 17:30 18.1.2024 23:59

Administrative Information

Previous Knowledge

inscription in the master`s program

Prerequisites Curriculum

See position in the curriculum


Knowledge of the state of the art in research in formal verification and testing.



Teaching Method

Interactive lectures either online or in the lecture hall

How to get a grade

written examination



Roderick Bloem


View more
Benedikt Maderbacher

PhD Student

View more