Verification and Testing

Course Number 705040 and 705041 | Wintersemester 2019/20

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 Slides
03.10.2019 Intro vt01-intro , vt01-cav2006
10.10.2019 Eraser & Locktree vt02 – concurrency
17.10.2019 Memory Debuggers vt03 – valgrind
24.10.2019 Symbolic Methods vt04 – SymbolicVerification
31.10.2019 Static Analysis vt05 – static checking
07.11.2019 Hoare Logic vt06 – hoare logic
14.11.2019 Hoare Logic (examples at the end of vt06) – solutions are published after the lecture
21.11.2019 SLAM I vt081 – SLAM – motivation and example

vt082 – SLAM – abstraction

28.11.2019 — No Lecture —
05.12.2019 SLAM II vt083 – SLAM – discovering predicates
12.12.2019 SLAM III
19.12.2019 — Christmas Holidays —
26.12.2019 — Christmas Holidays —
02.01.2020 — Christmas Holidays —
09.01.2020 Java Path Finder
16.01.2020 Current Research Topics
23.01.2020 Question Hour
30.01.2020 EXAM

Administrative Information

There will be a written exam at the end of the semester. Previous exams can be found in the PBS Online.

Please note that anyone with a TUG Online account can upload and modify the files there. Therefore we cannot provide any guarantees for their correctness. You can log in at this page with you TUG Online credentials.

Assignment Deadlines:

Assignment UE Handout UE Question Hour UE Deadline
A1 Locktree 10.10.2019 17.10.2019 and 18.10.2019 09:00 – 12:00 at seminarroom of IAIK 24.10.2019 27.10.2019
A2 Hoare 14.11.2019 21.11.2019 28.11.2019 01.12.2019
A3 SLAM 12.12.2019 09.01.2020 16.01.2020 *

* A3 needs to be submitted as hardcopy before the lecture on 16.01.2020!

Lecture Dates

Date Begin End Location Event Type Comment
2020/01/09 16:00 18:00 HS i1 Abhaltung VO fix/
2020/01/09 17:30 18:30 HS i1 Abhaltung UE fix/
2020/01/16 16:00 18:00 HS i1 Abhaltung VO fix/
2020/01/16 17:30 18:30 HS i1 Abhaltung UE fix/
2020/01/23 16:00 18:00 HS i1 Abhaltung VO fix/
2020/01/23 17:30 18:30 HS i1 Abhaltung UE fix/
2020/01/30 16:00 18:00 HS i1 Abhaltung VO fix/<a href="https://www.iaik.tugraz.at/course/verification-and-testing-705040-wintersemester-2019-20/">link</a>
2020/01/30 17:30 18:30 HS i1 Abhaltung UE fix/

Lecturers

Roderick Bloem
Roderick
Bloem

Professor

View more
Anja Felicitas Karl
Anja Felicitas
Karl

PhD student

View more
Erwin Heiner Peterlin
Erwin Heiner
Peterlin


View more