Summer School 2014: Verification Technology, Systems & Applications
The summer school on verification technology, systems & applications takes place at
the University of Luxembourg
from October 27-31, 2014. 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 verification can only be made
if all three aspects are considered as a whole. Our five speakers
Nikolaj Bjorner, Laura Kovács, Joel Ouaknine, Jaco van de Pol, and Helmut Veith
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, accommodation and daily living costs on their own. Recommendations on hotels can be found below.
Please apply electronically by sending an email to Eugen Denerz 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)
- a short statement if you want to contribute to the student sessions
until the 5th September 2014 (expired). Notifications on acceptance/rejection will be given by 15th September 2014 (expired).
The registration will be open to accepted applicants starting on 15th September 2014.
Student Grants for ICFEM 2014
Students who participate in the summer school may receive grants for the conference ICFEM 2014.
For further details and how to apply please visit the following website: http://icfem2014.uni.lu/grant.php
Please note that the application deadlines of the summer school and the student grants coincide.
All lectures will take place in room B001 in Weicker Building of SnT.
|Jaco van de Pol
|Jaco van de Pol
Student session (each 15 min)
- Evgeny Kotelnikov: Automated first-order reasoning for program analysis
- Li Li: Verifying timed security protocols
- Adrian Neumann: Certifying algorithms
- Vince Molnár: Saturation-based Incremental LTL Model Checking with Inductive Proofs
Student session (each 15 min)
- Ario Santoso: Verification of data-aware processes in the presence of ontologies
- Lydia Mattick: Towards automated compositional hardware/software co-verification
- Dan Zhang: Towards verified Java code generation from concurrent state machines
Student session (each 15 min)
- Daniel Darvas: Formal verification of industrial control systems at CERN
- Isabelle Mainz: State-space exploration of hybrid systems
- Ákos Hajdu: Extending the iteration strategy of the CEGAR approach on Petri Nets
- Heinrich Ody: Robust spatio-temporal logic for mobile agents
Note: The Student sessions give all participants the opportunity to discuss their PhD/Master topics with the speakers,
the organizers and further senior researchers. The topic can be introduced by a short talk (10 minutes) and/or a poster.
We encourage the participants to contribute to the student sessions. They are a great opportunity to discuss interesting topics
with world leading experts in a relaxing atmosphere.
Software Verification by Solving Horn Clauses
Satisfiability Modulo Theories (SMT) solvers offer a
compelling match for software tools, since several common software
constructs map directly into supported theories.
The lecture takes as starting point the state-of-the art SMT solver
Z3, developed at Microsoft Research. We revisit a central problem in
program analysis, model checking and verification - synthesizing
sufficient inductive invariants. It is formulated as solving
satisfiability of Horn clauses: We exploit that models of constrained
Horn clauses correspond directly to certificates of program
correctness. We examine algorithms used in software model checking as
strategies for solving Horn clauses. These algorithms include,
variants of bounded model checking, symbolic execution, bottom-up
saturation with finite relations, such as hash tables, BDDs and
three-valued bit-vectors, backwards chaining with tabling, fold-unfold
transformations, variants inspired by IC3 and interpolation
procedures. Z3 contains implementations of most of these algorithms
and they are used in various program and network analysis
Symbolic Computation and Theorem Proving in Program Analysis
Automatic understanding of the intended meaning of computer
programs is a very hard problem, requiring intelligence and reasoning.
During this lecture series, we will present a new method for program
analysis, called symbol elimination, that uses first-order theorem
proving and symbolic computation techniques to automatically discover
non-trivial program properties, such as loop invariants and loop
bounds. Moreover, symbol elimination can be used as an alternative to
interpolation for software verification.
We first describe how symbol elimination can be used for polynomial
and quantified invariant generation, by using Groebner basis
computation, quantifier elimination and saturation-based first-order
theorem proving. Next, we detail how Craig interpolants can be
automatically constructed and optimized from symbol eliminating
Symbol elimination is implemented in the award-winning first-order
theorem prover Vampire. We will discuss implementation details and
report on our experiments with using symbol elimination for generating
and proving intended safety properties of academic and industrial
A Survey of Program Termination: Practical and Theoretical Challenges
In the quest for program analysis and verification, program
termination -- determining whether a given program will always halt or
could execute forever -- has emerged as a pivotal
component. Unfortunately, this task was proven to be undecidable by
Alan Turing eight decades ago, before the advent of the first working
computers! In recent years, however, great strides were made in the
automated analysis of termination of programs, from simple counter
machines to Windows device drivers.
In this lecture, we will survey a cross section of topics ranging from
the history of program termination to the development of modern tools
such as Microsoft Research's Terminator, presenting in the process
some of the practical and theoretical challenges that remain and that
we expect will drive the field for the foreseeable future.
Jaco van de Pol
Scalable Multi-core Model Checking: Technology & Applications of Brute Force
Model checking realizes the dream of automated system and
software verification, improving system quality, avoiding disastrous
failures, and lowering development costs – or does it?
This course will focus on scalable multi-core model checking. I will
share the technological development that our research team at the
University of Twente has achieved over the last five years, in
concurrent data structures and parallel algorithms for model checking.
How to build a scalable model checker? It all starts with concurrent
data structures. In order to obtain ideal speedup, tens of processors
must be able to access data in shared memory in a correct manner,
without blocking each other at any time. For model checking, the
design of a shared hash table to store the large state space is
crucial. We managed to achieve ideal speedup up to 48 cores, even in
the presence of algorithms and representation techniques that achieve
enormous compression of state vectors.
The other ingredient is parallel algorithms. In order to speed up
complicated model checking tasks beyond reachability analysis we
developed a new method for liveness checking. Despite the inherent
complexity of parallelizing DFS, we propose Parallel Nested Depth
First Search. It is based on NDFS for LTL model checking. Parallel
workers apply random search by running their own NDFS. Conflicts due
to perturbed DFS orders will have to be avoided or repaired.
We will show how far multi-core model checking takes us when it comes
to applying symbolic techniques in model checking. In particular, we
can show successful experiments in parallel partial-order reduction,
parallel computations with Binary Decision Diagrams (BDD), and
parallel model checking of Timed Automata with a symbolic
representation of clock constraints. Finally, the course will show
real world applications that became possible by high-performance model
checking. We will see a variety of applications, ranging from railway
safety, analyzing PLC-like software, to systems biology.
In reality, big scale application of model checking is hampered by
limited scalability due to the state space explosion. Potential
solutions are state space reduction by exploiting symmetry or
abstraction, clever data structures and algorithms and by exploiting
brute-force computation resources.
Model Checking of Fault-Tolerant Distributed Algorithms
We recently introduced an abstraction method for
parameterized model checking of threshold-based fault-tolerant
distributed algorithms. The method requires understanding of several
verification techniques such as parametric abstraction, finite state
model checking and abstraction refinement.
In this course, we will describe how all these techniques interact in
order to achieve a possibly high degree of automation.
All participants are responsible for their own accommodation arrangements. Note: Luxembourg is a small country and some of the
below partner hotels may have released rooms for public bookings already, which means that availability and prices are no longer
guaranteed. We therefore strongly recommend you booking your accommodation as soon as possible!
You may contact hotels directly. Please find a list of hotels in the city of Luxembourg here.
In addition there is a youth hostel in Luxembourg City for budget travelers.
For your convenience, we have negotiated preferred rates with the hotels below.
To receive special rates for one of the hotels above please ...
- fill this form (with Adobe Reader or equivalent pdf viewer you can fill the form digitally),
- print it,
- sign it and
- submit it via email (after scanning) or by fax (see form sheet for more information).
Arrival / Directions
The Summer School 2014 will take place at the SnT at the University of Luxembourg.
Travelling to the SnT (University of Luxembourg)
General instructions can be found here. (It is the main office in the right upper corner on the map.)
Further instructions for people coming by car:
Parking places for visitors are on the -1 level in
the underground parking of Weicker building (in the red box of the image above). When you arrive at the entrance
of the parking, please ring at the gate. The guard will know about the visit
so he will open to you without any problems. People will need to take the lift
to go up from the underground parking to the ground floor (reception desk).
General Information on Location
Luxembourg has train connections to all of its neighboring countries: France, Germany and
Belgium. It is, however, also very feasible to travel by train when coming from the Nether-
lands 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
Belgium. A direct train goes once an hour between Brussels and Luxembourg. A
one-way ticket costs about 30 Euro. The train looks decent and modern, and the trip
Brussels-Luxembourg takes about 3 hours. Another possibility is to take the train
Li` ege-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.
Germany. Rail travelers 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 Saarbrucken,
a direct highway bus connection with Luxembourg (1 hour and 15 minutes) and the
tickets only cost 8 euro.
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.
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).
By far the most convenient way of air traveling 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 (for instance, one has to be
at the airport only one hour before departure). The national carrier LuxAir is 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. Our experience is that a taxi from the airport
to the city centre can cost 35 euro.
Frankfurt-Hahn airport and
are served by low-cost flights to many European
destinations. Flibco - a regular bus
the two airports to the main train station of the city of Luxembourg.
This regional airport is approximately 1.5 hours by public transport
from the City of Luxembourg. Unlike Frankfurt Hahn, there is no direct shuttle
bus, however, and travelers will need to change at least once.
An international driving licence is not necessary. Your home licence will suffice. Driving is on the right and wearing a seatbelt is required.
Driving in the city center 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. Free car parks are situated at the outskirts of
the city with a regular bus shuttle to the town center.
There is a frequent and efficient bus service which circulates throughout
Luxembourg City. The closest bus stop, named John F. Kennedy is
located within a one minute walk from the summer school venue. For details of all
national public transport options and schedule visit www.mobiliteit.lu.
From the airport you can take bus 16 to the summer school venue.
From the train station you can take the many busses:
The ticket can be bougth at the driver for 2€ that is valid for 2h. It is also possible to buy a carnet of 10-tickets for 16€.
Vel'oh ! - Bicycle renting stations
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 summer school site. A subscription for one week costs only 1€. The idea
is to 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 one euro per hour, after the
first 30 minutes, with a maximum of 5 Euro per day. Keep in mind that you’re allowed to
keep your rented bicycle for at most 24 hours.
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
Organization and Contact
- Stephanie Annet
- Pierre Fuhrer
- Magali Martin
For comments or questions send an email to Jun Pang
The summer school is organized by the Montefiore Institute, University of Luxembourg, INRIA Nancy, and the Max Planck Institute for Informatics Saarbrücken.
(Format is YYYY/MM/DD)
||2014/10/27 - 2014/10/31