Theoretical Foundations of Programming Languages

Seminar in Theoretical CS, Summer Semester 2016


  • 14.01.2015: we are online


13.04.2016, 16:00 Introduction at seminar room of i2 (E1, room 4201b)
09.05.2016 Detailed outline of report due
13.06.2016 Seminar report due
04.07.2016 Presentation slides due
18./19.07.2016 Seminar at seminar room of i2 (E1, room 4201b)



This seminar addresses several aspects of programming languages and systems, with emphasis on how principles underpin practical applications. Here the notion of “programming languages and systems” has to be understood in a broad sense; it ranges from sequential programming languages over concurrent and dynamic systems to logical approaches such as model checking. The previous, related seminar on Principles of Programming Languages provides a first overview of related topics.

Each area features a number of topics which are each covered by a scientific journal or conference article. These research articles are the basis on which students have to prepare their report and presentation.


Basic knowledge in the following areas is expected:

  • Formal languages and automata theory
  • Mathematical logic
  • Previous knowledge in semantics of programming languages, program analysis, model checking and/or concurrency theory is helpful but not mandatory


(The “B” and “M” tags respectively refer to topics on BSc and MSc level.)

Analysis of Pointer Programs

  1. B: Introduction to Separation Logic
  2. M: Separation Logic with Permissions
  3. M: Concurrent Separation Logic
  4. M: Compositional Shape Analysis
  5. M: Verification of Pointer Programs with Data by Forest Automata

Software Model Checking

  1. B: Abstraction in SMT-Based Unbounded Software Model Checking
  2. M: Configurable Software Verification
  3. M: Inductive Invariant Generation via Abductive Inference

Analysis of Probabilistic Systems

  1. B: Verification of Markov Decision Processes Using Learning Algorithms
  2. B: Parametric Probabilistic Reachability
  3. M: Fault Tree Analysis
  4. M: Multi-Objective Model Checking
  5. B: Interactive Markov Chains
  6. M: Analysis of Markov Automata

Schedule of Talks

Monday 18.07.2016
09:00-10:30 1, 2
10:45-12:15 4, 5
13:30-15:45 6, 8, 9
Tuesday 19.07.2016
09:00-11:15 10, 11, 14

Additional Material


Registration to the seminar is handled between January 14 and 27, 2016, via the central online form.


Thomas Noll <noll at>