Verification and Testing
Table of Content
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, valgrind_example |
| 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 | vt06 - hoare logic_solutions |
| 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 | vt084 - SLAM - Boolean Model Checking_withSolutions |
| 19.12.2019 | — Christmas Holidays — | |
| 26.12.2019 | — Christmas Holidays — | |
| 02.01.2020 | — Christmas Holidays — | |
| 09.01.2020 | Java Path Finder | vt09 - jpf |
| 16.01.2020 | Current Research Topics (not relevant for the exam) | Error Masking talk by Anja Felicitas Karl Abstractions For Error Masking talk by Benedikt MaderbacherMachine Learning by Masoud Ebrahimi |
| 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 | |
| A2 Hoare | 14.11.2019 | 21.11.2019 | |
| A3 SLAM | 12.12.2019 | 09.01.2020 | 16.01.2020 * |
Lecturers
Bloem
Professor