Building a Software Model-Checker
Model-checking techniques are being increasingly applied to software. In this course I will start by introducing jMoped, a tool for the analysis of Java programs. I will then proceed to explain the theory and algorithms behind the tool.

In jMoped we assume that variables have a finite range. I will start by considering the computational complexity of verifying different classes of programs satisfying this constraint. As we shall see, even in this case many verification problems can be undecidable. After choosing a reasonable class of programs, I will introduce a model-checking algorithm based on pushdown automata. Then I will address the problem of data: while variables have a finite range, this range may be large. I will present an approach to this problem based on BDDs.

Protocol Validation with mCRL
In most formal methods, data types are limited to say Booleans, natural numbers, lists. mCRL is a process algebraic language in which abstract data types are a first-class citizen. It is supported by a toolset that allows model checking as well as theorem proving. In this tutorial I will explain the basics of mCRL, algorithms for state space generation and minimization, a temporal logic for model checking, and a number of case studies.

Probabilistic Model Checking
Probabilistic model checking is a formal verification technique for the analysis of systems that exhibit stochastic behaviour. Such behaviour occurs, for example, due to randomisation, commonly used as a symmetry breaker in distributed coordination, security and communication protocols. Stochastic modelling is also important in performability, dependability and fault-tolerance, and more recently in the analysis of biological processes. Probabilistic model checking enables a range of quantitative analyses of probabilistic models against specifications such as "the worst-case probability of intrusion within 10 seconds", "the minimum expected power consumption over all possible schedulings", or "the expected time until a protein degrades". In recent years, increasing interest in the topic of probabilistic verification has led to significant advances in the applicability and efficiency of these techniques, as well as the discovery of interesting and anomalous behaviour in a wide range of real-life case studies.

This course will give an overview of the area of probabilistic model checking, covering both the theoretical foundations as well as the practical aspects of the topic. The lectures will include three types of probabilistic models (all variants of Markov chains), specification notations (based on probabilistic temporal logics), and techniques available for their automatic verification. The course will also introduce PRISM ( www.prismmodelchecker.org ), a state-of-the-art probabilistic model checker, and illustrate several case studies that have been modelled and analysed in PRISM, such as the Bluetooth device discovery, Zeroconf link-local addressing, power management, probabilistic contract signing, and biological signalling pathways.