University of Passau, Germany

CPAchecker is an open-source software-verification framework that is built on the concepts of Configurable Program Analysis (CPA). CPAchecker integrates most of the state-of-the-art technologies for software model checking as independent components in the framework. Examples are counterexample-guided abstraction refinement (CEGAR), lazy predicate abstraction, interpolation-based refinement, large-block encoding, and bounded model checking. Every abstract domain, together with the corresponding operations, implements the interface of configurable program analysis. The main algorithm is configurable to perform a reachability analysis on user-specified combinations of existing CPAs. In software verification, it takes a considerable amount of effort to convert a verification idea into actual experimental results --- we aim at accelerating this process. CPAchecker allows to study the influence of different concepts and ideas on the performance of the verification in isolation from other parameters, and we will demonstrate this on a few examples, in particular, using our predicate analysis.

Technische Universität Hamburg-Harburg

Cyber-physical systems are characterized by an IT infrastructure controlling effects in the physical world. Attacks are intentional actions that try to cause undesired effects in the physical world. We will examine to which extent traditional IT security techniques can protect against attacks on cyber-physical systems, and which additional measures could be deployed to strengthen their security.

Delft University of Technology

The cost of memory testing increases with every generation of new memory chips. New technologies are introducing new defect mechanisms that were unknown in the past. Precise fault modeling to design efficient tests is therefore essential in order to keep the test cost and test time within economically acceptable limits, while keeping a high product quality.
The objective is to provide attendees with an overview of fault modeling, test design and BIST for memory devices in the nano-era. Traditional fault modeling and recent development in fault models for current and future technologies are covered. Systematic methods are presented for designing and optimizing tests, supported by industrial results from different companies. Impact of algorithmic (e.g., data-background) and non-algorithmic (e.g. voltage) stresses is explored in order to get better insight in the test effectiveness. BIST architectures are covered; Finally, future challenges in memory testing (failure mechanism, test, diagnosis, etc) are highlighted.

Corpus Christi College Oxford

Quicksort is probably the most familiar and important randomised algorithm in computer science. It is well known that the expected number of comparisons on any input of $n$ distinct keys is asymptotically $2 n \ln n$. Crucially, the probability of a large deviation above this value is very small. This probability was well estimated in 1996 by Hayward and the speaker, with rather an ad-hoc proof: we shall revisit this result in the light of more recent results on concentration.

Aarhus University

Howard's algorithm (a.k.a. policy iteration) is a standard algorithm for solving Markov decision processes. Furthermore, generalizations of the algorithm solve various kinds of two-player games, including parity games, concurrent reachability games and Shapley's stochastic games. The worst case time complexity of the algorithm was until recently poorly understood, but in recent years, a surge of publications on the topic have given us an almost complete understanding of its complexity in the various settings in which it applies. We shall give a survey of these results and explain how they unexpectedly led to the answer to a classical open question concerning the complexity of a randomized variant of the simplex algorithm for linear programming. We shall also present the open problems that remain.

CNRS, Laboratoire d'Informatique de Grenoble

Secret sharing is a protocol, introduced independently by Shamir and Blakley, for distributing a secret among n players. A secret sharing protocol has a threshold k if any group of at least k players can recover the secret, whereas any group of at most k-1 players has no information about the secret. In this presentation, we will mainly focus on the case where the protocol is described by a graph and the shared secret is a quantum state (protocols introduced by Markham and Sanders). This family of graph-based protocols is very promising in terms of physical implementation. Unanimity graph-based protocols (i.e. the threshold is the total number of players) are known. We present quasi-unanimity protocols (the ratio k/n tends to 1 as n tends to infinity), and we prove the existence of protocols such that k<0.811n. This last result is proved using probabilistic methods (Lovasz Local Lemma) and is non-constructive, however we show that a random graph has a threshold at most 0.811n with high probability. Finally, we show that computing the threshold of a given graph is hard (the corresponding decision problem is NP-complete).

•