Verification and Testing (WS 2021/22)

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 (some old,some new)	old VideoS (2020/21)
07.10.2021	Intro		vt01-intro (updated)	vt-intro
14.10.2021	Eraser & Locktree	[1] [2]	vt02-concurrency	vt-concurrency
21.10.2021	Memory Debuggers	[3] [4][5]	vt03-valgrind	vt-valgrind
28.10.2021	Symbolic Methods		vt04-SymbolicVerification	vt-SymbolicVerification
04.11.2021	Hoare Logic	[6] [7][8]	vt05-hoare-logic	vt-hoare-logic
11.11.2020	Hoare Logic	[6] [7][8]	allHoareRules, vt05-hoare-logic2	vt-hoare-logic2
18.11.2021	Deductive Program Verification	[12]	vt07-deductive-verification	vt-deductive-verification
25.11.2021	Deductive Program Verification	[12]	dafny_examples (updated for both Dafny lectures)
02.12.2021	SLAM	[9] [10][11]	vt091-SLAM-motivation-and-example	vt-slam1
09.12.2021	SLAM	[9] [10][11]	vt092-SLAM-abstraction	vt-slam2
16.12.2021	SLAM	[9] [10][11]	vt093-SLAM-discovering-predicates, vt094-SLAM-Boolean-Model-Checking, SLAM_examples	vt-slam3
13.01.2021	Java Path Finder	[2]	vt08-jpf	vt-jpf
20.01.2021	Current Research Topics
27.01.2021	Question Hour

You can access the videos of this years lecture at TUbe (requires login). The live stream is also available there.

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] Memory Debuggers: Valgrind memcheck-manual (sec4.5). [4] Memory Debuggers: Valgrind memcheck2005.pdf. [5] Memory Debuggers: Valgrind shadow-memory2007.pdf. [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] 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. [10] 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. [11] 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. [12] 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 exercise descriptions will be handed out via git and submitting your work is also done there.

Calendar

Assignment	Handout	Question Hour	Deadline
A1 Locktree	18.10.2021	25.10.2021 16:00	02.11.2021 23:59
A2 Hoare	04.11.2021	15.11.2021 16:00	18.11.2021 23:59
A3 Dafny	25.11.2021	13.12.2021 16:00	16.12.2021 23:59
A4 SLAM	16.12.2021	17.1.2022 16:00	20.01.2022 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/sa.gruppen_einteilung?clvnr=259783&corg=983

Lecturers