Verification of Parallel Programs (VPP)
Lecturer: Prof. Dr. Marie-Christine Jakobs
Typically, the course is offered each winter term.
Current Course Information
Tu 2:00pm-3:00pm, Zoom, Question & Answering session
- VPP in TUCaN
- VPP material in Moodle
The course deals with mostly automatic verification approaches for multi-threaded programs with shared memory. Topics of the course are:
- Semantics of parallel programs, e.g., interleaving semantics
- Static and dynamic approaches for data race detection
- Techniques for deadlock detection
- Verification of program properties (e.g., with sequentialization, bounded model checking, etc.)
- Partial Order Reduction
- Thread-modular verification
At the end of the course, students can name a number of techniques for the verification of parallel programs, especially in the area of data race and deadlock detection as well as for verification of safety properties. They should be able to explain the underlying formalisms of the techniques, to describe the work flow of the different techniques, and to apply the techniques on examples. Moreover, the students know the strengths and weaknesses of the techniques.
Recommended Previous Knowledge
Knowledge according to the first four bachelor terms in computer science that is ideally supplemented by knowledge of automatic software verification techniques for sequential programs as taught in the course Automatic Software Verification.
- K. R. Apt, F. S. de Boer, E.-R. Olderog: Verification of Sequential and Concurrent Programs. Springer 2009.
Data Race Detection
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, T. E. Anderson: Eraser: A Dynamic Data Race Detector for Multi-Threaded Programs. SOSP 1997.
- E. Poznianski, A. Schuster: Efficient On-the-Fly Data Race Detection in Multithreaded C++ Programs. IPDPS 2003.
- C. Flanagan, S. N. Freund: FastTrack: efficient and precise dynamic race detection. PLDI 2009.
- Dawson R. Engler, Ken Ashcraft: RacerX: effective, static detection of race conditions and deadlocks. SOSP 2003.
- Mayur Naik, Chang-Seo Park, Koushik Sen, David Gay: Effective static deadlock detection. ICSE 2009.
- Akash Lal, Thomas W. Reps: Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. CAV 2008.
- Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. CAV 2014.
Bounded Model Checking
- L. C. Cordeiro, B. Fischer: Verifying multi-threaded software using SMT-based context-bounded model checking. ICSE 2011
- C. Flanagan, S. N. Freund, S. Qadeer: Thread-Modular Verification for Shared-Memory Programs. ESOP 2002
Partial Order Reduction
- D. Peled: Partial-Order Reduction. Handbook of Model Checking 2018.
- P. Godefroid, D. Pirottin: Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract). CAV 1993.
- P. Godefroid, P. Wolper: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. Formal Methods in System Design 2(2) 1993.
- C. Flanagan, S. N. Freund: Atomizer: a dynamic atomicity checker for multithreaded programs. POPL 2004