Summer School 2011: Verification Technology, Systems & Applications

VTSA11

The summer school on verification technology, systems & applications takes place at the Montefiore Institute (University of Liège) from September, 19th-23th, 2011. We believe that all three aspects verification technology, systems & applications strongly depend on each other and that progress in the area of formal analysis and verifiation can only be made if all three aspects are considered as a whole. Our five speakers Alessandro Armando, Franz Baader, Bruno Blanchet, Florent Jacquemard, and Joost-Pieter Katoen stand for this view in that they represent and will present a particular verification technology and its implementation in a system in order to successfully apply the approach to real world verification problems.

The number of participants in the school is limited to 40. We expect participants to hold a bachelor (or higher) degree in computer science (or equivalent) and to have basic knowledge in propositional and first-order logic.

The summer school is free of charge. It includes the lectures, daily coffee breaks and lunches and the special summer school dinner on Wednesday. Participants take travel, accomodation and daily living costs on their own. Recommendations on hotels can be found below.

Application

Please apply electronically by sending an email to vtsa11@montefiore.ulg.ac.be including

until the 22nd of July, 2011. Notifications on acceptance will be given by 12th of August, 2011.

Registration

The registration will be open to accepted applicants starting on 19th of August, 2011.

Program

All lectures will take place in room R3 at the Montefiore Institute.

Schedule

September 19
Monday
September 20
Tuesday
September 21
Wednesday
September 22
Thursday
September 23
Friday
9.00-12.30 Bruno Blanchet
Slides Intro
Slides ProVerif
Bruno Blanchet
Slides Intro
Slides ProVerif
Joost-Pieter Katoen
Slides Part 2
Florent Jacquemard
Slides
Alessandro Armando
Slides Part 1
12.30-14.00 Lunch break
14.00-17.20 Florent Jacquemard
Slides
Joost-Pieter Katoen
Slides Part 1
Franz Baader
Slides 1 2 3 4 5 6
Franz Baader
Slides 1 2 3 4 5 6
Alessandro Armando
Slides Part 2
17.30-18.30 Presentations by participants Presentations by participants Presentations by participants
Evening School Dinner

Lecturer(s)

Alessandro Armando
Alessandro Armando

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.

Franz Baader
Franz Baader

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.

Bruno Blanchet
Bruno Blanchet

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.

Florent Jacquemard
Florent Jacquemard

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.

Joost-Pieter Katoen
Joost-Pieter Katoen

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.

Accommodation

The participants are responsible for their room reservations.
Here is a map where most hotels are represented.
You can also have a look at informations provided by the tourism office.

Hotel Mercure
Price for single/double room 110/126 euros, breakfast included.
Please use this form.
Bd de la Sauvenière, 100
B-4000 Liège
Tel: + 32 (0) 4/221 77 11
Fax: + 32 (0) 4/221 77 01
Email: mercureliege@alliance-hospitality.com

Alliance Hotel Palais des Congrès
Price for single/double room 110/126 euros, breakfast included.
Please use this form.
Esplanade de l'Europe 2
B-4020 Liège
Tel: + 32 0) 4/342 60 20
Fax: + 32 (0) 4/343 48 10
Email: ahliege@alliance-hospitality.com

Best Western Univers Hotel
Price for single/double room 68/79 euros, breakfast included

To get this price, when booking a room please specify : "VTSA 2011-Universite de Liège".
When booking a room, also provide all the necessary credit card informations and DON'T use independent booking website (otherwise, it is not possible to have this special rate).
Rue des Guillemins 116
B-4000 Liège
Tel : + 32 (0) 4/254 55 55
Fax: + 32 (0) 4/254 55 00
Email: univershotel@skynet.be
www.univershotel.be

Husa de la Couronne
Price for a room 100 euros, breakfast included

To get this price, when booking a room please specify : "VTSA 2011-Universite de Liège".
When booking a room, also provide all the necessary credit card informations and DON'T use independent booking website (otherwise, it is not possible to have this special rate).
Place des Guillemins 11
B-4000 Liège
Tel: + 32 (0) 4/340 30 00
Fax: + 32 (0) 4/340 30 01
Email: info.couronne@husa.es
www.hotelhusadelacouronne.be

Hotel Ibis Liège Centre Opera
Price for single/double room 82/96 euros, breakfast included.
To get this price, when booking a room please specify : "VTSA 2011-Universite de Liège".
When booking a room, also provide all the necessary credit card informations and DON'T use independent booking website (otherwise, it is not possible to have this special rate).
Place de la République Française, 41
B-4000 Liège
Tel: + 32 (0) 4/230 33 33
Fax: + 32 (0) 4/223 04 81
Email: h0864@accor.com

Hotel les acteurs
Price for single/double room 74/81 euros, breakfast included.
To get this price, when booking a room please specify : "VTSA 2011-Universite de Liège".
When booking a room, also provide all the necessary credit card informations and DON'T use independent booking website (otherwise, it is not possible to have this special rate).
rue sur la Fontaine, 41
B-4000 Liège
Tel: + 32 (0) 4/223 00 80
Fax: + 32 (0) 4/221 19 48
Email: lesacteurs@skynet.be
www.lesacteurs.be

Arrival / Directions

The Summer School 2011 will take place at the Montefiore Institute (University of Liège).

Travelling to Liège

General instructions can be found on the Montefiore Institute location page.

Organization and Contact

General Organization

Local Organization

Website

For comments or questions send an email to Bernard Boigelot (boigelot (at) montefiore.ulg.ac.be).

The summer school is organized by the Montefiore Institute, University of Luxembourg, INRIA Nancy, and the Max Planck Insitute for Informatics Saarbrücken.

Important Dates

(Format is MM/DD/YYYY)

Sponsored by
INRIA MPII University of Lige Luxembourg
fnrs Moves SNT