Seminar in Theoretical CS, Summer Semester 2016

News

• 14.01.2015: we are online

Deadlines

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

1. 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
2. M: Separation Logic with Permissions
   • Literature: Bornat et al.: Permission accounting in separation logic
   • Supervisor: Thomas Noll
   • Student: Oliver Westphal
3. M: Concurrent Separation Logic
   • Literature: Viktor Vafeiadis: Concurrent separation logic and operational semantics
   • Supervisor: Thomas Noll
   • Student: –
4. M: Compositional Shape Analysis
   • Literature: Calcagno et al.: Compositional Shape Analysis by means of Bi-Abduction
   • Supervisor: Christoph Matheja
   • Student: Felix Frei
5. 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

6. 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
7. M: Configurable Software Verification
   • Literature: 
     • Beyer et al: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
     • Beyer et al.: Predicate Abstraction with Adjustable-Block Encoding
   • Supervisor: Tim Lange
   • Student: –
8. 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

9. 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
10. B: Parametric Probabilistic Reachability
    • Literature: Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang: Probabilistic reachability for parametric Markov models
    • Supervisor: Matthias Volk
    • Student: Dustin Jungen
11. 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
12. M: Multi-Objective Model Checking
    • Literature: Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis: Multi-objective Model Checking of Markov Decision Processes
    • Supervisor: Matthias Volk
    • Student: –
13. B: Interactive Markov Chains
    • Literature: H. Hermanns, J.-P. Katoen: The How and Why of Interactive Markov Chains
    • Supervisor: Hao Wu
    • Student: –
14. 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

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>