Reliably Secure Software Systems (RS3) –
DFG Priority Programme 1496

Tutorial 2012 (September 3-6, 2012)


The overall topics of this tutorial were Program Analysis and Verification.
The goal was to establish a common knowledge base and terminology
for collaborations. The target audience was PostDocs, PhD students, Master's students,
and Bachelor's students who are working on an RS3 project or are otherwise
associated with RS3.

Topics included:

  • Automata and Logics for Reactive Systems
  • Fundamentals of Program Analysis
  • From Simply-Type Lambda Calculus to ML Polymorphism
  • Local Constraint Solving
  • Model Checking Information Flow in Reactive Systems
  • Annotated Typing and Subtyping HM(X) as Implementation of Type-Based Analysis
  • Optimal Interprocedural Generation of Linear Program Invariants
  • Type-Based Analysis – A Type System for Access Control
  • Dynamic and Mixed Analysis: Gradual Types and Case Studies
  • Side-Effecting Constraint Systems
  • From Verification to Synthesis
  • Game Logics
  • Automata-Based Analysis of Recursive Concurrent Programs

Lectures were held by:

  • Prof. Bernd Finkbeiner, Ph.D. (Universität des Saarlandes)
  • Prof. Dr. Markus Müller-Olm (Westfälische Wilhelms-Universität Münster)
  • Prof. Dr. Peter Thiemann (Universität Freiburg)
  • Dr. Vesal Vojdani (TU München)

In addition to lectures, the tutorial also contained practical

Location and Schedule

The tutorial took place at Schloss Buchenau in the vicinity of Fulda (about 25 km, see travel details below), on September 3–6, 2012. The schedule can be found here.

At Schloss Buchenau there was full-board accommodation.

Arrival on the late afternoon of Sunday, September 2, is highly recommended. Departure is on Thursday, September 6 in the afternoon.


A description of how you can get to Schloss Buchenau is available on the website of Schloss Buchenau. The nearest train station is Bad Hersfeld (about 12 km to Schloss Buchenau).

In order to simplify your journey, you can sign up in the RS3 Wiki so that we can organize transport from Bad Hersfeld to Schloss Buchenau in groups of people who arrive roughly at the same time.

Application (closed)

The application deadline was July 23, 2012


If you have further questions concerning the tutorial, please send an e-mail to tutorial at