Verification and Testing

Course Number 705040 and 705041 | Wintersemester 2020/21

Lecturers

Roderick Bloem

Benedikt Maderbacher

Teaching Assistants

Erwin Heiner Peterlin

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 Teams Papers Slides Video
01.10.2020 Intro link vt01-intro vt-intro
08.10.2020 Eraser & Locktree link [1] [2] vt02-concurrency, vt02-concurrency_notes vt-concurrency
15.10.2020 Memory Debuggers link [3] [4][5] vt03-valgrind vt-valgrind
22.10.2020 Symbolic Methods link vt04-SymbolicVerification, vt04-SymbolicVerification_notes vt-SymbolicVerification
29.10.2020 Hoare Logic link [6] [7][8] vt05-hoare-logic vt-hoare-logic
05.11.2020 Hoare Logic link [6] [7][8] allHoareRules, vt05-hoare-logic2 vt-hoare-logic2
12.11.2020 Static Analysis link vt06-static-checking vt-static-checking
19.11.2020 Deductive Program Verification link [12] dafny_examples, vt07-deductive-verification vt-deductive-verification
26.11.2020 Java Path Finder link [2] vt08-jpf vt-jpf
03.12.2020 SLAM link [9] [10][11] vt091-SLAM-motivation-and-example vt-slam1
10.12.2020 SLAM link [9] [10][11] vt092-SLAM-abstraction vt-slam2
17.12.2020 SLAM link [9] [10][11] vt093-SLAM-discovering-predicates, vt094-SLAM-Boolean-Model-Checking, SLAM_examples vt-slam3
14.01.2021 Current Research Topics link
28.01.2021 Question Hour link

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.
You should receive your repository soon.

upstream

Calendar

Assignment Handout Question Hour Deadline
A1 Eraser 08.10.2020 16.10.2020 22.10.2020 29.10.2020
A2 Hoare 29.10.2020 06.11.2020 12.11.2020 13.11.2020
A3 Dafny 20.11.2020 27.11.2020, 04.12.2020 11.12.2020 17.12.2020
A4 SLAM 17.12.2020 15.01.2021 21.01.2021

If you have problems with adding the git remote, try to use https instead of ssh.
Use the following code to do so:

git remote add -f upstream https://extgit.iaik.tugraz.at/scos/scos.teaching/scos.teaching.vt/vt2020/vt-sources.git

Administrative Information

IMPORTANT-INFORMATION

The lectures will be held via Microsoft Teams.

You can join using the Chrome web browser to join anonymous, or register an account and use the desktop client.

Exercise Question Hours: Friday at 11am on Discord. You can join the server using https://discord.gg/nsPGRthhEz.

Lecture Dates

Date Begin End Location Event Type Comment
2021/01/28 16:00 18:00 External Location (please check TUGRAZonline) Abhaltung VO fix/https://teams.microsoft.com/l/meetup-join/19%3ameeting_YTRhYjc5OGMtNDVjNi00ZmJkLTllYjEtYTU3MmZjMjZhMzhh%40thread.v2/0?context=%7b%22Tid%22%3a%22ed101a69-657e-4069-a6c5-d163430b82da%22%2c%22Oid%22%3a%22774c2ff4-7e61-4193-a947-b241235cd0e6%22%7d

Lecturers

Roderick Bloem
Roderick
Bloem

Professor

View more
Benedikt Maderbacher
Benedikt
Maderbacher

PhD Student

View more

Teaching Assistants

Erwin Heiner Peterlin
Erwin Heiner
Peterlin