Verification and Testing (WS 2024/25)

Course Number 705040 | Wintersemester 2024/25

Lecturers

Roderick Bloem

Benedikt Maderbacher

Teaching Assistants

Julian Koppensteiner

Sebastian Puck

Content

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

Material

The slides can be found here: https://cloud.tugraz.at/index.php/s/eDoMHT8ExBo7PMc.
DATE TOPIC Papers Slides
03.10.2024 Intro see cloud
10.10.2024 Eraser & Locktree [1], [2]
17.10.2024 no lecture
24.10.2024 Memory Debuggers [3], [4]
31.10.2024 Java Path Finder [2]
07.11.2024 Symbolic Methods
14.11.2024 Hoare Logic I [5],[6],[7],[8]
21.11.2024 Hoare Logic II [5],[6],[7],[8]
28.11.2024 Dafny [9]
05.12.2024 SLAM I [10],[11],[12]
12.12.2024 SLAM II [10],[11],[12]
19.12.2024 SLAM III [10],[11],[12]
09.01.2025 Security
16.01.2025 Current Research Topics & Question Hour

Resources

[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] AdressSanitizer: Serebryany, K., Bruening, D., Potapenko, A., & Vyukov, D. AddressSanitizer: A Fast Address Sanity Checker, 2012 USENIX Annual Technical Conference
[4] MemorySanitizer: Stepanov, E., & Serebryany, K. MemorySanitizer: fast detector of uninitialized memory use in C++, 2015 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)
[5] Hoare Logic: Hoare-Logic course .
[6] Hoare Logic: Hoare-Logic course .
[7] Hoare Logic: Hoare-Logic Uni Trier (German) .
[8] Hoare Logic: F. Wotawa,Einführung in die InformatikSkriptum,pp. 157-171,(German), Oktober 2002.
[9] Dafny: K. Rustan M. Leino Dafny: An Automatic Program Verifier for Functional Correctness., LPAR-16, International Conference on Logic for Programming Artificial Intelligence and Reasoning, LNCS 6355, pp. 348-370, 2010
[10] SLAM: T. Ball, S. K. Rajamani, Bebop:A Symbolic Model Checker for Boolean Programs, SPIN 2000 Workshop on Model Checking of Software, LNCS 1885, pp. 113-130, August/September 2000.
[11] SLAM: T. Ball, S. K. Rajamani, Automatically Validating Temporal Safety Properties of Interfaces, SPIN 2001, Workshop on Model Checking of Software, LNCS 2057, pp. 103-122, May 2001.
[12] SLAM: T. Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. Automatic Predicate Abstraction of C Programs, In Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation (PLDI '01). ACM, New York, NY, USA, 203-213, 2001.

Exercises

Tutorials

Topic Date Materials
Abstract syntax trees 10.10.2024
Z3 SMT solver 14.11.2024

Assignments

Assignment Handout Question Hour Deadline
A1 Eraser 10.10.2024 24.10.2024 17:30 31.10.2024 23:59
A2 Hoare 14.11.2024 28.11.2024 17:30 05.12.2024 23:59
A3 Dafny 28.11.2024 12.12.2024 17:30 19.12.2024 23:59
A4 SLAM 19.12.2024 09.01.2025 17:30 16.01.2025 23:59

Administrative Information

Previous Knowledge

inscription in the master`s program

Prerequisites Curriculum

See position in the curriculum

Objective

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

Language

English

Teaching Method

Interactive lectures either online or in the lecture hall

How to get a grade

written examination

Registration

https://online.tugraz.at/tug_online/ee/rest/pages/slc.tm.cp/course-registration/530229

Lecture Dates

Date Begin End Location Event Type Comment
2024/10/10 16:00 18:00 HS i1 Abhaltung VO fix/
2024/10/10 17:30 18:30 HS i1 Abhaltung UE fix/
2024/10/17 17:30 18:30 HS i1 Abhaltung UE fix/
2024/10/17 17:30 18:30 HS i1 Abhaltung UE fix/
2024/10/23 17:00 18:00 HS i6 Abhaltung UE fix/
2024/10/24 16:00 18:00 HS i1 Abhaltung VO fix/
2024/10/24 17:30 18:30 HS i1 Abhaltung UE fix/
2024/10/31 16:00 18:00 HS i1 Abhaltung VO fix/
2024/10/31 17:30 18:30 HS i1 Abhaltung UE fix/
2024/11/07 16:00 18:00 HS i1 Abhaltung VO fix/
2024/11/07 17:30 18:30 HS i1 Abhaltung UE fix/
2024/11/14 16:00 18:00 HS i1 Abhaltung VO fix/
2024/11/14 16:00 18:00 HS i12 "DynaTrace Hörsaal" Abhaltung VO fix/
2024/11/14 17:30 18:30 HS i12 "DynaTrace Hörsaal" Abhaltung UE fix/
2024/11/14 17:30 18:30 HS i1 Abhaltung UE fix/
2024/11/21 16:00 18:00 HS i1 Abhaltung VO fix/
2024/11/21 16:00 18:00 HS i1 Abhaltung VO fix/
2024/11/21 17:30 18:30 HS i1 Abhaltung UE fix/
2024/11/28 16:00 18:00 HS i1 Abhaltung VO fix/
2024/11/28 17:30 18:30 HS i1 Abhaltung UE fix/
2024/12/05 16:00 18:00 HS i1 Abhaltung VO fix/
2024/12/05 17:30 18:30 HS i1 Abhaltung UE fix/
2024/12/12 16:00 18:00 HS i1 Abhaltung VO fix/
2024/12/12 17:30 18:30 HS i1 Abhaltung UE fix/
2024/12/19 16:00 18:00 HS i1 Abhaltung VO fix/
2024/12/19 17:30 18:30 HS i1 Abhaltung UE fix/
2025/01/09 16:00 18:00 HS i1 Abhaltung VO fix/
2025/01/09 17:30 18:30 HS i1 Abhaltung UE fix/
2025/01/16 16:00 18:00 HS i1 Abhaltung VO fix/
2025/01/16 17:30 18:30 HS i1 Abhaltung UE fix/
2025/01/21 10:00 18:00 HS i6 Abhaltung UE fix/
2025/01/22 13:00 18:00 HS i5 Abhaltung UE fix/
2025/01/23 16:00 18:00 HS i1 Abhaltung VO fix/
2025/01/23 17:30 18:30 HS i1 Abhaltung UE fix/
2025/01/30 16:00 18:00 HS i1 Abhaltung VO fix/
2025/01/30 17:30 18:30 HS i1 Abhaltung UE fix/

Lecturers

Roderick Bloem
Roderick
Bloem

Professor

View more
Benedikt Maderbacher
Benedikt
Maderbacher

PhD Student

View more

Teaching Assistants

Julian Koppensteiner
Julian
Koppensteiner


View more
Sebastian Puck
Sebastian
Puck


View more