Verification and Testing (WS 2023/24)

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

DATE	TOPIC	Papers	Slides
05.10.2023	Intro
12.10.2023	Eraser & Locktree
19.10.2023	Memory Debuggers
09.11.2023	Symbolic Methods
16.11.2023	Hoare Logic I
23.11.2023	Hoare Logic II
30.11.2023	SLAM I
07.12.2023	SLAM II
14.12.2023	SLAM III
11.01.2024	Java Path Finder
18.01.2024	Current Research Topics & Question Hour

Resources

Exercises

Calendar

Assignment	Handout	Question Hour	Deadline
A1 Locktree	12.10.2022	25.10.2022 17:00	03.11.2022 23:59
A2 Hoare	16.11.2022	30.11.2022 17:30	14.12.2022 23:59
A3 SLAM	14.12.2022	11.1.2023 17:30	18.1.2023 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/407778

Lecture Dates

Date	Begin	End	Location	Event	Type	Comment
2023/10/05	16:00	18:00	HS i1	Abhaltung	VO	fix/
2023/10/12	16:00	18:00	HS i1	Abhaltung	VO	fix/
2023/10/12	16:00	18:00	HS i1	Abhaltung	VO	fix/
2023/10/12	17:30	18:30	HS i1	Abhaltung	UE	fix/
2023/10/19	16:00	18:00	HS i1	Abhaltung	VO	fix/
2023/10/19	17:30	18:30	HS i1	Abhaltung	UE	fix/
2023/10/25	17:00	18:00	HS i6	Abhaltung	UE	fix/
2023/11/09	16:00	18:00	HS i1	Abhaltung	VO	fix/
2023/11/09	17:30	18:30	HS i1	Abhaltung	UE	fix/
2023/11/16	16:00	18:00	HS i1	Abhaltung	VO	fix/
2023/11/16	17:30	18:30	HS i1	Abhaltung	UE	fix/
2023/11/23	16:00	18:00	HS i3 "LENZING Hörsaal"	Abhaltung	VO	fix/
2023/11/23	17:30	18:30	HS i1	Abhaltung	UE	fix/
2023/11/30	16:00	18:00	HS i1	Abhaltung	VO	fix/
2023/11/30	17:30	18:30	HS i1	Abhaltung	UE	fix/
2023/12/07	16:00	18:00	HS i1	Abhaltung	VO	fix/
2023/12/07	17:30	18:30	HS i1	Abhaltung	UE	fix/
2023/12/07	17:30	18:30	HS i1	Abhaltung	UE	fix/
2023/12/14	16:00	18:00	HS i1	Abhaltung	VO	fix/
2023/12/14	17:30	18:30	HS i1	Abhaltung	UE	fix/
2024/01/11	16:00	18:00	HS i1	Abhaltung	VO	fix/
2024/01/11	17:30	18:30	HS i1	Abhaltung	UE	fix/
2024/01/18	16:00	18:00	HS i1	Abhaltung	VO	fix/
2024/01/18	17:30	18:30	HS i1	Abhaltung	UE	fix/
2024/01/23	10:00	18:00	HS i6	Abhaltung	UE	fix/
2024/01/24	13:00	18:00	HS i5	Abhaltung	UE	fix/
2024/01/25	16:00	18:00	HS i1	Abhaltung	VO	fix/
2024/01/25	17:30	18:30	HS i1	Abhaltung	UE	fix/

Lecturers