Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Course INF-56-51-K-6

Concurrency Theory (4V+2U, 8.0 LP)

Course Type

SWS Type Course Form CP (Effort) Presence-Time / Self-Study
- K Lecture with exercise classes (V/U) 8.0 CP 156 h
4 V Lecture 56 h
2 U Exercise class (in small groups) 28 h
(4V+2U) 8.0 CP 84 h 156 h

Basedata

SWS 4V+2U
CP, Effort 8.0 CP = 240 h
Position of the semester 1 Sem. in WiSe
Level [6] Master (General)
Language [EN] English
Lecturers
Area of study [INF-ALG] Algorithmics and Deduction
Livecycle-State [NORM] Active

Possible Study achievement

  • Verification of study performance: proof of successful participation in the exercise classes (ungraded)
  • Details of the examination (type, duration, criteria) will be announced at the beginning of the course.

Contents

  • 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

Literature

Will be announced during the lecture.

Requirements for attendance (informal)

None

Requirements for attendance (formal)

None

References to Course [INF-56-51-K-6]

Module Name Context
[INF-56-51-M-6] Concurrency Theory P: Obligatory 4V+2U, 8.0 LP
Course-Pool Name
[INF-Alg_V-KPOOL-6] Lectures of the teaching area Algorithmics and Deduction