Virtual Reality WiSe 2026/27

Verification of Parallel Programs WS 2026/27

Enrollment Key: VerParProg 26/27

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.

Literature

Program Semantics

  • 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.

Deadlock Detection

  • 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.

Sequentialization

  • 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

Thread-modular Verification

  • 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.

Atomicity Checking

  • C. Flanagan, S. N. Freund: Atomizer: a dynamic atomicity checker for multithreaded programs. POPL 2004

Uncertainty in Artifical Intelligence and Machine Learning WiSe 2026/27

Quantum Applications WiSe 2026/27

Diese Vorlesung findet im Wintersemester 2026/2027 leider nicht statt.

Program Analysis for Security WiSe26/27

Parallel and High Performance Computing WiSe 2026/27

Methods in Software Engineering WiSe 2026/27

Diese Vorlesung findet aller Voraussicht nach nicht statt!

Machine Learning WiSe 2026/27

IT-Sicherheit WiSe 2026/27

Intelligent Systems WiSe 2026/27

Grid und Cloud Computing WiSe 2026/27

Deep Learning and Artificial Intelligence WiSe 2026/27

Data Mining Algorithms 1 WiSe 2026/27

Category Theory WiSe 2026/27

Automated Theorem Proving WiSe 2026/27

Automated theorem proving is a subfield of mathematical logic that concerns itself with proving mathematical theorems fully automatically using computer programs. These programs are called automated theorem provers. They can be used as standalone programs to solve logic problems or in tandem with interactive theorem provers (also called proof assistants) to discharge proof obligations that arise.

In this course, we will review some of the main approaches to automated theorem proving. The course focuses on the _theory_ of theorem proving. Stylistically, the course has a mathematical flavor (with definitions, lemmas, proofs, etc.).

Self-enrollment key: ATP202627

Advanced Topics in Computer Graphics WiSe 2026/27