Summer School 2010: Verification Technology, Systems & Applications

VTSA08

The third summer school on verification technology, systems & applications takes place at the University of Luxembourg from September, 06th-10th, 2010. 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 Javier Esparza, Wan Fokkink, Marta Kwiatkowska, Markus Müller-Olm, and Wang Yi 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, free lunches and the special summer school dinner on Wednesday. Apart from that, participants have to 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 Jun Pang (jun.pang (at) uni.lu) including

until the 23th of July, 2010. Notifications on acceptance will be given by 6th of August, 2010.

Registration

The registration will be open to accepted applicants starting on the 6th of August, 2010.

Program

All lectures will take place in Auditoire Tavenas (Campus Limpertsberg, University of Luxembourg).

Schedule

September 06
Monday
September 07
Tuesday
September 08
Wednesday
September 09
Thursday
September 10
Friday
9.00-12.30 Wang Yi
Part 1 Part 2 Part 3
Marta Kwiatkowska
Part 1 Part 2
Marta Kwiatkowska
Part 3 Part 4
Markus Müller-Olm
All Slides
Wan Fokkink
All Slides
12.30-14.00 Lunch break
14.00-17.20 Wang Yi
Part 4 Part 5
Markus Müller-Olm
All Slides
Wan Fokkink
All Slides
Javier Esparza
Part 0 Part 1
Javier Esparza
Part 2 Part 3
17.30-18.30 Presentations by participants Presentations by participants Presentations by participants Drinks
Evening School Dinner
19.30

Lecturer(s)

Javier Esparza
Javier Esparza

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.

Wan Fokkink
Wan Fokkink

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.

Marta Kwiatkowska
Marta Kwiatkowska

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.

Markus Müller-Olm
Markus Müller-Olm

Fundamentals of Software Model Checking
It is an old dream of computer science to verify the correctness of software systems by fully automatic means. Despite of well-known fundamental limits uncovered by the theory of computability, there has been great progress in the study of automatic methods for semantic analysis of software in the last decades. In particular it has been studied how to apply model checking to software. Model checking verifies temporal-logic specifications by exhaustive state-space exploration. In this lecture I will present important fundamental insights and techniques developed for software model checking.

Wang Yi
Wang Yi

Modeling and Analysis of Timed Systems
I will provide a tutorial on model checking of real-time systems with a focus on semantical and algorithmic aspects of verification tools. The main topics include:

  • Transition systems and temporal Logics
  • Theory of timed systems: timed automata and decision problems
  • UPPAAL: input languages, algorithms and data structures
  • TIMES: from timed models to code with guarantees on real-time properties
I will also summarize our recent work on real-time applications on multicores including technical challenges and new results on timing and schedulability analysis for multicore real-time software.

Accommodation

The participants are responsible for their room reservations.
Most people will probably prefer to stay in the city centre and take the bus to the university's campus at Limpertsberg.

The above list is by no means meant to be complete. More information about hotels and other things can be found at the Luxembourg City Tourist Office.

Arrival / Directions

Summer School Site

Salle Tavenas
Campus Limpertsberg

The VTSA Summer School 2010 will be held at the Campus Limpertsberg of the University of Luxembourg, in the Tavenas room (Salle Tavenas, 102 Avenue Pasteur, L-2311 Luxembourg). To get there, take bus 3 and get off at the end of the line (Lycée Technique Michel-Lucius). From the bus stop, walk in the direction that the bus is facing. After a few hundred meter down the street, you will see on your left hand side the former monastery where the summer school is held.

Bus tickets come in two forms:

Both one-way tickets and day cards are available on the bus itself (€ 1,50 and € 4, respectively). It is also possible to buy a carnet of 10 one-way tickets (€ 12) or 5 daycards (€ 16) at newspaper stands (like for instance at the airport or railway station). Tickets bought in advance (carnet) need to be stamped in the bus. Many of the city buses have stamping machines; if your bus does not, then ask the driver to simply write the time and date on your ticket.

When planning to go by public transport, one can use the online travel planner, which covers the entire country. Of particular interest is bus 3, which goes to the summer school site. It can be useful to have a printout of its route and timetable. Keep in mind, however, that bus 3 does not stop at the railway station (Gare).

Another interesting local transport alternative is to move around by bicycle. The City of Luxembourg has several fully automated bicycle rental stations, including one that is nearby the conference site. A subscription for one week costs only € 1. The idea is take a bicycle from one rental station and return it to perhaps another. If the trip takes less than 30 minutes, it's for free. Otherwise one starts to pay € 1 euro per hour, after the first 30 minutes, with a maximum of € 5 per day. Please keep in mind that you're allowed to keep your rented bicycle for at most 24 hours.

We also advise participants to buy a detailed map that covers the entire City of Luxembourg, at either the airport or railway station, since the summer school is located at the edge of the city (north-east).

WiFi will be available at the summer school site itself, the City of Luxembourg also provides a WiFi facility in the city center, as well as at the airport and railway station.


View VTSA2010 in a larger map

Travelling to Luxembourg

By airplane

Luxembourg has its own airport, but it is also possible to use one of the airports in the region.

By train

Luxembourg has train connections to all of its neighbouring countries: France, Germany and Belgium. It is, however, also very feasible to travel by train when coming from the Netherlands or the UK. When planning train travel in Europe, the website of Deutsche Bahn is an excellent source of information, since they have a travel planner that covers pretty much entire Europe.

By Coach

Those travelling on a budget might want to be aware that the City of Luxembourg is also served by Eurolines. There also used to be a Eurolines office in the city centre, but it appears to be closed now.

By car

Driving in the city of Luxembourg is not always a pleasant experience, partly due to the fact that many streets are one-way. Also, not every hotel offers parking space. Those who are nevertheless willing to drive can comfort themselves with the fact the Luxembourg has some of the lowest petrol prices in the EU.

Organization and Contact

General Organization

Local Organization

Website

For comments or questions send an email to Jun Pang (jun.pang (at) uni.lu).

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

VTSA 10

Important Dates

(Format is MM/DD/YYYY)

Sponsored by
INRIA MPII Luxembourg SNT Fonds National Recherche Luxembourg