Module INF-56-51-M-6

Concurrency Theory (M, 8.0 LP)

Module Number	Module Name	CP (Effort)
INF-56-51-M-6	Concurrency Theory	8.0 CP (240 h)

CP, Effort	8.0 CP = 240 h
Position of the semester	1 Sem. in WiSe
Level	[6] Master (General)
Language	[EN] English
Module Manager	Schweitzer, Pascal, Prof. Dr. (PROF \| DEPT: INF)
Lecturers	Zetzsche, Georg, Dr. (WMA \| DEPT: INF)
Area of study	[INF-ALG] Algorithmics and Deduction
Reference course of study	[INF-88.79-SG] M.Sc. Computer Science
Livecycle-State	[NORM] Active

Type/SWS	Course Number	Title	Choice in Module-Part	Presence-Time / Self-Study		SL	SL is required for exa.	PL	CP	Sem.
4V+2U	INF-56-51-K-6	Concurrency Theory	P	84 h	156 h	U-Schein	ja	PL1	8.0	WiSe

About [INF-56-51-K-6]: Title: "Concurrency Theory"; Presence-Time: 84 h; Self-Study: 156 h
About [INF-56-51-K-6]: The study achievement [U-Schein] proof of successful participation in the exercise classes (ungraded) must be obtained. It is a prerequisite for the examination for PL1.

The grade of the module examination is also the module grade.

Multithreaded programs
- Petri nets
- safety and liveness properties
- Petri nets invariants and linear programming
- Forward analysis: Karp & Miller tree
- Backward analysis: well structured transitions systems (WSTS)
Message passing programs
- Communicating state machines with FIFO or lossy channels
- Process algebra and the actor model
- Reduction to WSTS
GPU Programs
- Bulk synchrony
- Small model property
- Reduction to sequential program verification

The students develop operational models for systems with multiple components interacting concurrently.
The students understand correctness properties and algorithms to verify these properties.
The students will apply existing techniques on examples and adapt them to related classes of systems.

Will be announced during the lecture.

None