Seminar in Theoretical CS, Summer Semester 2016

### News

- 14.01.2015: we are online

### Deadlines

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) |

### Overview

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.

### Prerequisites

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

### Topics

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

#### Analysis of Pointer Programs

- B: Introduction to Separation Logic
**Literature:**Peter O’Hearn: A Primer on Separation Logic (and Automatic Program Verification and Analysis)**Supervisor:**Thomas Noll**Student**: Benjamin Hirsch

- M: Separation Logic with Permissions
**Literature:**Bornat et al.: Permission accounting in separation logic**Supervisor:**Thomas Noll**Student**: Oliver Westphal

- M: Concurrent Separation Logic
**Literature:**Viktor Vafeiadis: Concurrent separation logic and operational semantics**Supervisor:**Thomas Noll**Student**: –

- M: Compositional Shape Analysis
**Literature**: Calcagno et al.: Compositional Shape Analysis by means of Bi-Abduction**Supervisor**: Christoph Matheja**Student**: Felix Frei

- M: Verification of Pointer Programs with Data by Forest Automata
**Literature:**Abdulla et al.: Verification of heap manipulating programs with ordered data by extended forest automata**Supervisor:**Christoph Matheja**Student**: Fabian Schneider

#### Software Model Checking

- B: Abstraction in SMT-Based Unbounded Software Model Checking
- Literature: Komuravelli et al.: Automatic Abstraction in SMT-Based Unbounded Software Model Checking
- Supervisor: Tim Lange
- Student: Fabian Heimbürger

- M: Configurable Software Verification
- M: Inductive Invariant Generation via Abductive Inference
**Literature:**Dillig et al.: Inductive Invariant Generation via Adductive Inference**Supervisor:**Tim Lange**Student:**Andreas Heuvels

#### Analysis of Probabilistic Systems

- B: Verification of Markov Decision Processes Using Learning Algorithms
**Literature:**Kretinsky et al.: Verification of Markov decision processes using learning algorithms**Supervisor:**Christian Dehnert**Student**: Stephan Kölker

- B: Parametric Probabilistic Reachability
**Literature:**Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang: Probabilistic reachability for parametric Markov models**Supervisor:**Matthias Volk**Student**: Dustin Jungen

- M: Fault Tree Analysis
**Literature:**Hichem Boudali, Pepijn Crouzen, Mariëlle Stoelinga: A Rigorous, Compositional, and Extensible Framework for Dynamic Fault Tree Analysis**Supervisor:**Matthias Volk**Student**: Niklas Reinker

- M: Multi-Objective Model Checking
- B: Interactive Markov Chains
**Literature:**H. Hermanns, J.-P. Katoen: The How and Why of Interactive Markov Chains**Supervisor:**Hao Wu**Student**: –

- M: Analysis of Markov Automata
**Literature:**D. Guck, H. Hatefi, H. Hermanns, J.-P. Katoen, M. Timmer: Analysis of Timed and Long-Run Objectives for Markov Automata**Supervisor:**Hao Wu**Student**: Mariia Mentiu

### 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

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

### Contact

Thomas Noll <noll at cs.rwth-aachen.de>