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.
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.
The registration will be open to accepted applicants starting on the 6th of August, 2010.
All lectures will take place in Auditoire Tavenas (Campus Limpertsberg, University of Luxembourg).
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
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.
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
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:
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.
- 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
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
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.
Travelling to Luxembourg
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,
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).
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
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.
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
(Format is MM/DD/YYYY)
- Application Deadline: 07/23/2010
- Notification until: 08/06/2010
- Summer School: 09/06/2010 - 09/10/2010