-
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
Module INF-56-51-M-6
Concurrency Theory (M, 8.0 LP)
Module Identification
Module Number | Module Name | CP (Effort) |
---|---|---|
INF-56-51-M-6 | Concurrency Theory | 8.0 CP (240 h) |
Basedata
CP, Effort | 8.0 CP = 240 h |
---|---|
Position of the semester | 1 Sem. in WiSe |
Level | [6] Master (General) |
Language | [EN] English |
Module Manager | |
Lecturers | |
Area of study | [INF-ALG] Algorithmics and Deduction |
Reference course of study | [INF-88.79-SG] M.Sc. Computer Science |
Livecycle-State | [NORM] Active |
Courses
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.
Examination achievement PL1
- Form of examination: oral examination (20-60 Min.)
- Examination Frequency: Examination only within the course
- Examination number: 65651 ("Concurrency Theory")
Evaluation of grades
The grade of the module examination is also the module grade.
Contents
Competencies / intended learning achievements
- 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.
Literature
Will be announced during the lecture.
Requirements for attendance (informal)
Modules:
Requirements for attendance (formal)
None
References to Module / Module Number [INF-56-51-M-6]
Course of Study | Section | Choice/Obligation |
---|---|---|
[INF-88.79-SG] M.Sc. Computer Science | Computer Science Theory | [WP] Compulsory Elective |
[INF-88.79-SG] M.Sc. Computer Science | Formal Fundamentals | [WP] Compulsory Elective |
[INF-88.79-SG] M.Sc. Computer Science | Specialization 1 | [WP] Compulsory Elective |
[MAT-88.105-SG] M.Sc. Mathematics | Subsidiary Topic (Minor) | [WP] Compulsory Elective |