IFIP WG 2.2 Meeting Lisbon

September 23-26, 2013

Titles and slides of the talks

(in chronological order)

Erika Ábrahám
Modeling and Analysis of Hybrid Systems

Andrzek Murawski
Deconstructin General References via Game SemanticsTBA

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

Javier Esparza

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

Michele Boreale
An Introduciont to Quantitative Inforamtion Flow (QIF)

Marjan Sirjani

Pawel Sobocinski
Nets with Boundaries

Abstract: 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

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

Naoki Kobayaschi
On Properties of Higher-Order Languages

Uwe Nestmann
On Full Abstraction

Peter D. Mosses
Editor Support for Formal Specifications

Ahmed Bouajjani
Verification of Concurrent Programs: Decidability, Complexity, Reductions

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

Maciej Koutny
Synthesis of Tissue Systems

Luis Caires
Behavioral Separation Types at Work