**Erika Ábrahám**- Modeling and Analysis of Hybrid Systems

PDF **Andrzek Murawski**- Deconstructin General References via Game SemanticsTBA

PDF **Barbara König**- Graph Specification Languages and Applications to the
Verification of Graph Transformation Systems

PDF **Javier Esparza**- TBA

**K.V.S. Prasad**- Controlled Languages and Machine Translation by GF: A Brief Introduction

PDF , Grammatical Framework Website **Ernst Rüdiger Olderog**- Proving Safety of Traffic Manoeuvres on
Country Roads

PDF **Michele Boreale**- An Introduciont to Quantitative Inforamtion Flow (QIF)

PDF **Marjan Sirjani**- TBA

**Pawel Sobocinski**- Nets with Boundaries

PDFAbstract: We present a compositional algebra of Petri nets, inspired by string diagrams used in mathematics and physics, that allows all nets to be expressed as a composition of a small number of basic net components. We argue that the resulting language allows the capture of distribution within a Petri net, which can be used to improve performance of model checking.

**Viorica Sofroni-Stokkermans**- Modularity in Automated Reasoning and
in the Verification of Complex Systems

PDF **Radu Grosu**- Uniform Lasso Sampling

Abstract: In many practice-relevant applications, storing all states of a probabilistic system in memory is infeasible, and model checking tools break down. However, it is often the case that one can compute the successors of any given state in an efficient way. This opens up the door to sampling based approaches, which search the state space of the system for lassos offending the linear temporal property of interest. Unfortunately, such techniques are in general unable to sample the lasso space in a uniform way, which not only leads to inefficient search, but also hampers drawing any conclusion, in case no offending lasso is found. In this talk I will show that if one can (over)estimate the number of lassos in the system, one can devise a search technique that very accurately approximates uniform lasso sampling, with minimal memory requirements.

**Masahiko Sato**- Viewing λ-Terms through Maps

PDF **Naoki Kobayaschi**- On Properties of Higher-Order Languages

PDF **Uwe Nestmann**- On Full Abstraction

PDF **Peter D. Mosses**- Editor Support for Formal Specifications

PDF **Ahmed Bouajjani**- Verification of Concurrent Programs: Decidability, Complexity,
Reductions

PDF **Antonin Kucera**- Patrolling Games

Patrolling is one of the central problems in operational security. Formally, a patrolling problem is specified by a set U of vulnerable targets and a function d which to every target u assigns the time d(u) ∈ N needed to complete an intrusion at u. The goal is to design an optimal strategy for a defender who is moving from target to target and aims at detecting possible intrusions. The defender can detect an intrusion at u only by visiting u before the intrusion is completed. The goal of the attacker is to maximize the probability of a successful attack. We assume that the attacker is adversarial, i.e., he knows the strategy of the defender and can observe her moves. We assume that all targets are equally important and that each move from target to target takes one unit of time.

We show that the defender has an optimal strategy for every patrolling problem. We also show that an optimal defender's strategy may require both memory and randomization, and may (inevitably) employ irrational probabilities.

**Einar Broch Johnsen**- Engineering Virtualized Services

PDF **Maciej Koutny**- Synthesis of Tissue Systems

PDF **Luis Caires**- Behavioral Separation Types at Work

PDF