**Ernst-Rüdiger Olderog**- Petri Games: Synthesis of Distributed Systems with Causal Memory

SlidesWe present a new multiplayer game model for the interaction and the flow of information in a distributed system, developed with Bernd Finkbeiner. The players are tokens on a Petri net. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the causal history of the other player. We show that for Petri games with a single environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy for the system players is EXPTIME-complete. We also report about the tool ADAM developed by Manuel Gieseking that implements the new game solving algorithm and case studies performed with it.

**Pawel Sobocinski**- Control Theory Meets Operational Semantics

Slides **Markus Müller-Olm**- Automata-Based Analysis of Threaded Programs

Slides **Joseph Sifakis**- Rigorous System Design

Slides **Naoki Kobayashi**- Program Verification via Higher-Order Model Checking

Slides **Igor Walukiewicz**- A Model for Behavioural Properties of Higher-Order Programs

Slides **Parosh Abdulla**- Verifying Linearizability

Slides **Luke Ong**- On Static Analysis of Resource-Bounded Pi-Calculus

Slides **Jean-Francois Raskin**- Non-zero Sum Games for Reactive Synthesis

Slides **Luis Caires**- Logic and Types, Concurrency and Non Determinism

Slides **Uwe Nestmann**- Dynamic Causality (in Event Structures)

Slides **Rocco De Nicola**- Languages and Calculi for Collective Adaptive Systems

Slides **Javier Esparza**- Verification of Population Protocols

Slides **Frank de Boer**- OpenJDK's Java utils.Collection.sort() is Broken

SlidesThese slides present the correctness of TimSort, which is the main sorting algorithm provided by the Java standard library. The goal is functional verification with mechanical proofs. During our verification attempt we discovered a bug which causes the implementation to crash. We characterize the conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise the performance. We formally specify the new version and mechanically verify the absence of this bug with KeY, a state-of-the-art verification tool for Java.

**Ahmed Bouajjani**- Refinement Checking for Libraries of Concurrent Objects

Slides **Matthew Hennessy**- Behavioural Equivalences for Co-operating Transactions

Slides