Session 1: The Rewriting Approach to Decision Procedures
Program analysis and automated verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisfiability of sets of ground literals in decidable, first-order theory $T$. The rewrite approach to decision procedures amounts to using the well-known superposition-based inference system for first-order equational logic for deciding satisfiability in various theories of interest in verification (including the theory of lists, encryption, extensional arrays, extensional finite sets, and their combinations). This tutorial provides an introduction to the rewrite approach to decision procedures and also shows that, contrary to the folklore, a general-purpose prover non only can compete but can also outperform ad-hoc decision procedures with built-in theories, thereby showing that the rewriting approach is not only elegant and conceptually simple, but has important practical implications.

Session 2: Automatic Symbolic Analysis of Access Control Policies
In computer systems access control policies specify who can access which resources. If on the one hand, policies must guarantee that a minimal set of users can access certain resources (principle of least privilege), on the other hand, they should be flexible enough to to support a wide range of application scenarios. For this reason, the traditional models for access control (such as Role-Based Access Control, RBAC) have been extended in several ways, e.g. with delegation and with rules for policy administration (Administrative RBAC, ARBAC). All these aspects make the analysis of access control policies so complex to make manual inspection of the policy unfeasible. Automated analysis techniques are thus of paramount importance to check security policies against desired security requirements. This tutorial introduces an approach to the automatic analysis of access control policies that leverages recent symbolic model checking for infinite state systems and state-of-the-art theorem proving techniques.

Reasoning in Description Logics
Description Logics (DLs) are a successful family of logic-based knowledge representation formalisms, which can be used to represent the conceptual knowledge of an application domain in a structured and formally well-understood way. They are employed in various application domains, such as natural language processing, configuration, and databases, but their most notable success so far is the adoption of the DL-based language OWL DL as standard ontology language for the semantic web.

This tutorial concentrates on designing and analyzing reasoning procedures for DLs. After a short introduction and a brief overview of the research of the last 20 years, it will on the one hand present approaches for reasoning in expressive DLs, which are the foundation for reasoning in OWL DL. On the other hand, it will consider reasoning in the more light-weight DLs EL and DL-Lite, which are the foundation for the more tractable OWL 2 profiles OWL 2 EL and OWL 2 QL.

Automatic Verification of Security Protocols: the verifier ProVerif
After a brief overview of the field of automatic protocol verification, we will focus on the tool ProVerif. This verifier can verify a wide range of security properties of the protocols, such as secrecy, authentication, and limited cases of process equivalences, in a fully automatic way. It supports cryptographic primitives defined by rewrite rules or by certain equations. Furthermore, the obtained security proofs are valid for an unbounded number of sessions of the protocol, in parallel or not. ProVerif relies on an abstract representation of the protocol by a set of Horn clauses, and on a resolution algorithm on these clauses. We will explain this algorithm.

Tree automata techniques for the verification of infinite state-systems
Tree automata are an appropriate formalism for the verification of safety properties of programs and systems whose states can be represented by tree structures. This the case for instance of networks of communicating processes with a tree architecture, functional programs manipulating tree data values with pattern matching, imperative programs with recursive procedure calls and thread creation, transformations of XML documents...

In this tutorial, we will present classes of tree automata over ranked and unranked trees, and their properties and decision procedures interesting in the context of verification. We will also present how their expressiveness can be extended with some constraints, and by considering tree languages modulo equational theories.

Verification and Abstraction of Continuous-Time Markov Models
Continuous-time Markov chains (CTMCs) are omnipresent. They are used as semantical backbone of Markovian queueing networks, stochastic Petri nets, stochastic process algebras, and calculi for systems biology.

The lectures will focus on the analysis of CTMCs using model checking. Both temporal-logic based model checking as well as (timed) automata-based model checking will be considered. Equivalences and pre-orders are covered and we'll discuss which logical fragments are preserved by them. Finally, we introduce three-valued abstraction on CTMCs, and apply it to the analysis of examples from systems biology and (large) queueing networks. As outlook, we'll discuss recent progress on the analysis of continuous-time Markov decision processes.