Summer School 2010: Verification Technology, Systems & Applications

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

a one page CV
an application letter explaining your interest in the school and your experience in the area
a copy of your bachelor certificate (or equivalent or a more significant certificate)

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		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		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		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		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		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.

Golden Tulip Central Molitor
The big advantage of this hotel is that it is very near to the railway station (5 minutes walk), and thus very suitable for those arriving by train. There's a direct bus to the summer school site (bus 3) with a bus-stop right in front of the hotel.
Mercure Hotel Alfa is right in front of the railway station. When leaving the hotel, walk to the left for the nearest bus stop of bus 3.
Hôtel Français
Located inside of the pedestrian zone, at one of the main squares of the city centre, Hôtel Français is a 3 minutes walk away from the downtown bus station ("Hamilius), from which a direct bus goes to the summer school site. When taking bus 16, get out at Royal. From the railway station ("Gare") to the downtown bus station takes 5 minutes by bus or 15 to 20 minutes by foot.
Hôtel Victor Hugo
Located just outside of the city centre, this hotel is in the same neighbourhood (Limpertsberg) as the summer school site, and it is probably best just to walk (about 20 minutes) instead of waiting for the bus. The city centre is just a 5 minutes walk away. When coming from the airport, take bus 16 to "Fondation Pescatore". (This hotel should not be confused with the 4-star Grand Hotel Victor Hugo - they are opposite each other)
For those travelling on a tight budget, we should at least mention the Luxembourg Youth Hostel, which is spotlessly clean, just like the rest of the country. Prices start at € 20. Although the hostel appears to be nearby the city centre when viewed on the map, one has to keep in mind that it lies in a steep valley and can be a bit difficult to reach (ask the staff for details).
Hotel Parc Belle Vue
Located in the center of the city. Currently, there is a special summer offer from July 16 to September 12, 2010.

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

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:

One way tickets, valid within the city of Luxembourg of a period up to two hours.
Day cards, valid for all trains and buses in the entire country

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.

Lux Airport. By far the most convenient way of air travelling to Luxembourg is to arrive at the national airport. The airport has recently been reconstructed and the shiningly new terminal indeed looks very appealing. Some of the advantages of Lux Airport are its relatively small size and fast and efficient procedures (one has to be at the airport only one hour before departure). Only a limited number of airlines fly to Luxembourg, including budget airline VLM (now called CityJet). The national carrier LuxAir is also a very decent option. From the airport, it's only 20 minutes to the city centre by bus. A good choice is to take bus 16 (route and timetable), which stops nearby all hotels mentioned later on this web page (€ 1.50 one-way). Our experience is that a taxi from the airport to the city centre can easily cost € 35.
Frankfurt Airport. Germany's largest airport is 3 hours and 45 minutes away from Luxembourg by train. A return ticket costs about 120 euro, less if one has a discount card from the German railways. Usually one has to change trains in Koblenz. Detailed travel schemes can be found on the website of Deutsche Bahn.
Frankfurt Hahn. Several budget airlines fly to this German regional airport, that is one hour and 45 minutes away from Luxembourg by shuttle bus. Expect to pay about € 30 for a bus return ticket Frankfurt Hahn - Luxembourg. This is one of the favourite options of the staff at the University of Luxembourg.
Saarbrücken Airport. This regional airport is approximately 3 hours by public transport from the City of Luxembourg. Unlike Frankfurt Hahn, there is no direct shuttle bus, however, and travellers will need to change at least once. To see your precise connection to Luxembourg, consult the online travel planner (From: "Flughafen, Saarbrücken Ensheim (SCN)" / To: "Luxembourg Gare").
Brussels Airport. The advantage of Brussels Airport is that it is connected to the Belgian railway network with its own station, located in the basement of the airport terminal. Expect to pay € 65 for a return ticket to Luxembourg (trains go every hour), a journey that takes about 3 hour and 30 minutes one way.
Charleroi Airport. This regional airport in the south of Belgium, sometimes also called "Brussels South Airport" hosts Ryanair as well as several other budget airlines. The airport doesn't have its own railway station, travellers first have to take the bus to the city of Charleroi, from where it is a 2 hours and 30 minutes journey to Luxembourg (change trains in Namur).

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.

Belgium. A direct train goes once an hour between Brussels and Luxembourg. A one-way ticket costs € 31. The train looks decent and modern, and the trip Brussels-Luxembourg takes about 3 hours. Another possibility is to take the train Liège-Luxembourg, which might be more direct for some parts of Belgium, but it has to be mentioned that this train makes a lot of stops.
France. Rail connections between France and Luxembourg were greatly improved with the opening of the new TGV Paris-Luxembourg. The trip takes just over 2 hours, with stopovers in Metz and Thionville.
Germany. Rail travellers coming from Germany can use the railway between Trier and Luxembourg. Trier, however, is a relatively small city and is not served by the ICE-network. The nearest German city on the ICE-network is Saarbrücken, which has a direct highway bus connection with Luxembourg (1 hour and 15 minutes).
The Netherlands. Train tickets from the Netherlands to Luxembourg can be bought at the domestic counter or even from the standard NS ticket vending machines (press "Belgium / Luxembourg"). When buying a ticket one has to specify whether one is going over Roosendaal-Brussels or over Maastricht-Liège. As most people of the Netherlands are probably aware of, the opening of fast train connection to Belgium and France (HSL) is being delayed and delayed. As a result of this, the existing train connection between Amsterdam and Brussels has been running for longer than its technical life expectancy, with various defects and trouble as a result. The second class can be crowded, so it does make some sense to try to buy a first class ticket. A standard return ticket from the Netherlands to Luxembourg does not have an exact return date on it (one just has to return within 2 months) which allows for some flexibility.
United Kingdom. Going from the UK to Luxembourg by train is actually a quite viable option. It is possible to buy a Eurostar ticket (to Brussels) that is valid to any station in Belgium. In that case, one may want to use this ticket until Arlon, the last station in Belgium before the border with Luxembourg. The additional return ticket Arlon-Luxembourg can be bought at the railway station in Brussels (where you can also ask whether conditions are still the same since our university staff used this possibility). Although flying is faster, taking the train has the advantage of being able to see something of the countryside. And it's also better for your CO2 footprint.

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.