
Rohit Chadha
Probabilistic models and their analysis
The use of randomization in concurrent or distributed systems is often key to achieving certain objectives. For example, it is used in distributed algorithms to break symmetry and in cryptographic protocols to achieve semantic security. While analyzing such systems for correctness, these systems are often modeled as transition systems that have both randomized and nondeterministic transitions. It is customary to resolve the nondeterminism by a scheduler who chooses a transition based on the past sequence of states visited during the computation. When analyzing such systems for correctness, it is often necessary to restrict the set of schedulers to obtain sound and precise results. The feasibility of the analysis depends on the class of schedulers under consideration. In this talk, we survey recent results on analysis of probabilistic systems focusing on restriction of schedulers that arise a) in reactive systems and b) in security protocols.

Thomas Colcombet
Asymptotic analysis of tropical automata
Automata weighted over tropical semirings (min,+) and (max,+) are useful modelling tools. Tropical automata compute maps from words to nonnegative integers (or infinity). Such maps are defined over a given input as the minimum/maximum over all accepting runs of the sum of weights of the transitions (each transition is weighted by a nonnegative integer in our case). (min,+)automata are naturally used to optimize computations over an input, and (max,+)automata naturally model worst case behaviours. Another classical application of tropical automata is the approximation probablistic automata.
It is known from D. Krob in the ninetees that the problem of comparing the maps definable by such automata (toward equality or order) is not decidable. In this talk, I will present several results that circumvent this difficulty, and give precise decidable approximations of these problematic problems. Our results essentially take the form of effective asymptotic descriptions of the behaviour of the automata when their inputs become arbitrarily large.
In particular, our result concerning (max,+)automata can be used for the analysis of the complexity of programs as a functions of the size of their inputs, thanks to the use of the size change abstraction.
These works are the subject of the PhD thesis of Laure Daviaud, defended this year, and part of them were the subject of a publication with Florian Zuleger. This research was funded by the ERC project GALE.

Barbara König
WellStructured Graph Transformation Systems
Graph transformation systems (GTSs) can be seen as wellstructured
transition systems (WSTSs), thus obtaining decidability results for
certain classes of GTSs. It was shown that wellstructuredness can be
obtained using the minor ordering as a wellquasiorder. We extend
this idea to obtain a general framework in which several types of GTSs
can be seen as (restricted) WSTSs. We instantiate this framework with
the subgraph ordering and the induced subgraph ordering. Furthermore
we present the tool UNCOVER and discuss runtime results.

Roland Meyer
Robustness against Relaxed Memory Models
For performance reasons, modern multiprocessors implement relaxed memory
consistency models that admit outofprogramorder and nonstore atomic
executions.
While data racefree programs are not sensitive to these relaxations,
they pose a serious problem to the development of the underlying
concurrency libraries.
Library routines that work correctly under Sequential Consistency (SC)
show undesirable effects when run under a relaxed memory model.
These routines are not robust against the relaxations that the processor
supports.
To enforce robustness, the programmer has to add safety net instructions
to the code that control the hardware  a task that has proven to be
difficult, even for experts.
We recently developed algorithms that check and, if necessary, enforce
robustness against prominent relaxed memory models like TSO implemented
in x86 processors and Power implemented in IBM architectures.
Given a program, our algorithms decide whether the actual behavior on
the processor coincides with the SC semantics.
If this is not the case, they synthesize safety net instructions that
enforce robustness.
When built into a compiler, our algorithms thus hide the relaxed memory
model from the programmer and provide the illusion of Sequential
Consistency.
In this talk, we motivate the robustness problem and explain how to
reduce it to a standard SC reachability query.

Ranko Lazic
Multidimensional energy games and related problems
I shall present recent work on multidimensional energy games, which
happen to have strong connections to several questions about vector addition systems, regarding finitesystem simulations, zeroreachability games and alternating termination.
The work is joint with Marcin Jurdzinski and Sylvain Schmitz.

Anca Muscholl
Walking With Data: Where Does it Stop?
Data formalisms apply to numerous settings where the reasoning in volves explicit comparisons of object identities.
Such formalisms are usually based on automata or logics that have the ability to compare data from an unbounded domain.
In the realm of databases, data may take the meaning of attribute values. In program verification, data may represent identities of processes,
communication channels, pointers or any other resource that can be of interest in the analysis of programs with dynamic objects.
This talk will survey several models of logics and automata with data and analyse their limits in decidability regarding fundamental
questions such as nonemptiness (satisfiability) and inclusion (containment). We will focuss on recently considered data formalisms
such as datawalking automata and Datalog, that are promising models regarding the above problems.

Ashutosh Trivedi
BoundedRate MultiMode Systems Based Motion Planning
Hybrid automata are a natural and expressive formalism to model systems that exhibit both discrete and continuous behavior.
However, the applications of hybrid automata in analyzing cyberphysical systems have been rather limited due to
undecidability of simple verification problems such as reachability.
This drawback of hybrid automata has fueled the investigation of the socalled compositional methodology
to design complex system by sequentially composing wellunderstood lowerlevel components.
This methodology has, for example, been used in the context of the motion planning problem for mobile robots,
where the task is to move a robot along a prespecified trajectory with arbitrary precision
by sequentially composing a set of wellstudied simple motion primitives,
such as "move left", "move right" and "go straight".
In this talk, we summarize some of our recent results related to efficient solution of motion planning problem
for systems whose motion primitives are given as constantrate vectors with uncertainties.

Thomas Wies
Ideal Abstractions of Concurrent Infinite State Systems
Many concurrent infinite state systems can be seen as wellstructured transition systems (WSTS). Examples include concurrent programs with sharedmemory and dynamic thread creation, as well as distributed message passing systems in the actors framework. WSTS are an attractive class of systems for formal analysis because they admit generic decision procedures for important verification problems such as coverability. Unfortunately, these decision procedures often have very high complexity or provide termination guarantees only in special cases that are not of practical relevance. To obtain a practical analysis with
more general termination guarantees, we propose an abstract interpretation that is inspired by decision procedures for the covering problem of WSTS. The abstract domain of our analysis builds on the ideal completion of the wellquasiordered state space to obtain an efficient symbolic representation of infinite sets of states. A widening operator that mimics accelerationbased forward algorithms for computing covering sets ensures termination while controlling the loss of precision of the analysis. I will present an instance of our analysis framework for the class of depthbounded systems and its application to verifying progress properties of concurrent data structure implementations.