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, semantics of selected weak memory models
- 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
- Verification with weak memory guarantees
- Dozent*in: Marie-Christine Jakobs