IFIP WG 2.2 Meeting Lucca

September 21-23, 2015

Titles and slides of the talks

(in chronological order)

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

We 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

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

Joseph Sifakis
Rigorous System Design

Naoki Kobayashi
Program Verification via Higher-Order Model Checking

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

Parosh Abdulla
Verifying Linearizability

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

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

Luis Caires
Logic and Types, Concurrency and Non Determinism

Uwe Nestmann
Dynamic Causality (in Event Structures)

Rocco De Nicola
Languages and Calculi for Collective Adaptive Systems

Javier Esparza
Verification of Population Protocols

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

These 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

Matthew Hennessy
Behavioural Equivalences for Co-operating Transactions