Verification and Testing (WS 2022/23)

Course Number 705040 | Wintersemester 2022/23

Lecturers

Teaching Assistants

Sebastian Puck

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
Deductive Software Verification with Dafny
Boolean Model Checking with the SLAM algorithm

Material

DATE	TOPIC	Papers	Slides
06.10.2022	Intro		vt01-intro
13.10.2022	Eraser & Locktree	[1] [2]	vt02 - concurrency
20.10.2022	Memory Debuggers	[3] [4]	vt03-memory_debugging
27.10.2022	Symbolic Methods		vt04 - SymbolicVerification
03.11.2022	Hoare Logic	[6] [7][8]	vt05 - hoare logic
10.11.2022	Hoare Logic		Chapters 2.1.10 and 5.1-5.4 in [6].
17.11.2022	Deductive Program Verification	[9]	dafny_examples.zip
24.11.2022	SLAM		vt081 - SLAM - motivation and example
01.12.2022	SLAM		vt082 - SLAM - abstraction
15.12.2022	SLAM		vt083 - SLAM - discovering predicates vt084 - SLAM - Boolean Model Checking
12.01.2023	Java Path Finder		vt07-jpf.pdf
19.01.2023	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) [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

Exercises

The assignments will be made available on our git repository: upstream You will receive your own git repository shortly, it will be used to submit your work.

Calendar

Assignment	Handout	Question Hour	Deadline
A1 Eraser	13.10.2022	20.10.2022 15:00	27.10.2022 23:59
A2 Hoare	03.11.2022	10.11.2022 15:00	17.11.2022 23:59
A3 Dafny	17.11.2022	24.11.2022 15:00	9.12.2022 23:59
A4 SLAM	15.12.2022	12.1.2023 16:00	19.1.2023 23:59