Personal tools

BadGriesbach 2015

From PUMA Graduiertenkolleg

Jump to: navigation, search

General Information

The PUMA workshop 2015 takes place in Bad Griesbach ( from October 19th (Monday) at 3 pm to October 23rd (Friday). The meeting takes place together with RiSE.



The workshop is organized at the Hotel Residenz. It is located at Prof-Baumgartner-Str 1, 94086 Bad Griesbach i. Rottal.

Getting there

  • The closest train station to Bad Griesbach is in Karpfham.
  • The program will start at 15:00, and there will be lunch at the hotel beforehand, so we think it is best to arrive at about 13:00-13:30.
  • To get from Karpfham station to the hotel (ca 6km), you could call a taxi (for example Taxi Hohenwarter at 00498532/3555).
  • For groups of several people, the hotel offered to provide a shuttle service. Write us an email in advance and we will arrange this if you are interested.

from Munich

  • To get there, take a train from Munich Central Station to Mühldorf (Oberbayern) and change to a train to Karpfham there.
  • For example, use the RB Munich-Mühldorf at 10:07 and change to the RB Mühldorf-Passau at 11:36. You will arrive in Karpfham at 12:48.
  • In Bavaria, a Bayern Ticket is probably the cheapest option, especially for groups of several people.

from Linz

  • Take a train from Linz Central Station to Passau and change to a train to Karpfham there.
  • For example, use the ICE Linz-Passau at 10:17 and the RB Passau-Mühldorf at 11:59. You will arrive in Karpfham at 13:07.

from Salzburg

  • Take a train from Salzburg Central Station to Mühldorf (Oberbayern) and change to a train to Karpfham there.
  • For example, use the IC Salzburg-Wien at 9:12. Change in Wels to the ICE to Frankfurt. Change in Passau to the RB to Mühldorf. You will arrive in Karpfham at 13:07.


  • Students from PUMA and RiSE are required to give a talk; postdocs may give a talk if they wish to. Each talk consists of 15 min presentation + 5 min discussion.
  • Professors can also give talks of variable length (to be agreed upon with the organisers).
  • There will be three invited talks
  • There will be a social event/excursion on one of the afternoons.

A preliminary version of the program can be found here: File:Schedule long.pdf. The book of abstracts of the talks can be found here: File:Abstract book.pdf.


Invited speakers

Name Presentation Title
Barbara Jobstmann Quantitative Objectives In Reactive Synthesis
David Monniaux How do we find invariants?
Igor Walukiewicz The Distributed Synthesis Problem

Participants from PUMA

Name Presentation Title
Professors Tobias Nipkow Uniform Proofs of Functional Correctness of Search Tree Data Structures
Javier Esparza An SMT Approach to Coverability and Fair Termination Analysis
Martin Hofmann The Probabilistic Powerdomain
PhD students Christian Müller Universal Information Flow using Self-Composition
Sabine Bauer Decidable Linear Tree Constraints
Christian Neukirchen Proof by Reflection for Decision Procedures with Certificates
Stefan Schulze-Frielinghaus   Inter-Procedural Two-Variable Herbrand Equalities
Salomon Sickert Deterministic ω-Automata for LTL: A Safraless, Compositional and Mechanically Verified Construction
Fabian Immler A Verified Enclosure for the Lorenz Attractor
Silvia Magdici Occupancy Prediction for Arbitrary Road Network in Automated Driving
Christoph-Simon Senjak An Implementation of Deflate in Coq
Albert Rizaldi Formalising Traffic Rules for Accountability of Autonomous Vehicles
Philipp Hoffmann Summarizing Cyclic Negotiations
Manuel Eberl Verified Asymptotic Analysis of Divide \& Conquer Recurrences
Julian Kranz Control Flow Graph Reconstruction of Binary Code
Ralf Vogler Proving Absence of Starvation by Means of Abstract Interpretation and Model Checking
Stephan Barth Parametric Path Compression Automata for Deciding Monadic Second Order Logic

Participants from RiSE

Name Presentation Title
Martin Chmelik Optimal Cost Almost-Sure Reachability in POMDPs
Laura Kovacs
Christoph Kirsch
Roopsha Samantha
Ana Sokolova Local Linearizability
Ayrat Khalimov Warehouse Full of Robots: Parameterized Synthesis
Thomas Henzinger
Ezio Bartocci
Martina Seidl
Krishnendu Chatterjee
Uwe Egly
Florian Zuleger Liveness of Parameterized Timed Networks
Nicolas Braud-Santoni
Przemyslaw Daca Statistical Model Checking for Unbounded Temporal Properties
Robert Koenighofer Synthesizing Adaptive Test Strategies for Reactive Systems from Temporal Logic Specifications
Andreas Fellner Don’t Care Abstraction
Martin Aigner Evaluating Fast, Multicore-Scalable, Low-Fragmentation Memory Allocation through Rigorous Performance Analysis in the Loop
Armin Biere
Thorsten Tarrach From Non-Preemptive to Preemptive Scheduling using Synchronization Synthesis
Helmut Veith
Roderick Bloem
Mirco Giacobbe Abstraction Refinement of Hybrid Systems using Support Functions
Florian Lonsing Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
Sebastian Arming Complexities of Repair Checking and Consistent Query Answering
Tatjana Petrov
Radu Grosu
Anna Lukina Model Checking as Control: Feedback Control for Statistical Model Checking of Cyber-Physical Systems
Sergiy Bogomolov