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
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.
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.
| October 27 Monday |
October 28 Tuesday |
October 29 Wednesday |
October 30 Thursday |
October 31 Friday |
|
|---|---|---|---|---|---|
| 9.00-12.30 | Joel Ouaknine |
Laura Kovács |
Laura Kovács |
Jaco van de Pol |
Nikolaj Bjorner |
| 12.30-14.00 | Lunch break | ||||
| 14.00-17.20 | Joel Ouaknine |
Helmut Veith |
Helmut Veith |
Nikolaj Bjorner |
Jaco van de Pol |
| 17.30-18.30 |
Student session (each 15 min)
|
Student session (each 15 min)
|
Student session (each 15 min)
|
Farewell drinks | |
| Evening | School dinner | ||||
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.
Nikolaj Bjorner
|
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
applications.
|
Laura Kovács
|
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
first-order proofs.
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
benchmarks.
|
Joel Ouaknine
|
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. |
Helmut Veith
|
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.
Hotel Parc Belle-Vue (3 stars)
5 Avenue Marie-Thérèse,
2132 Luxembourg
Hotel Parc Plaza (4 stars)
5 Avenue Marie-Thérèse,
2132 Luxembourg
To receive special rates for one of the hotels above please ...
The Summer School 2014 will take place at the SnT at the 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).
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 entire Europe.
Luxembourg airport. 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 Brussels-Charleroi airport are served by low-cost flights to many European destinations. Flibco - a regular bus service connects the two airports to the main train station of the city of Luxembourg.
Saarbrucken Airport. 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: 1, 16, 120, 125, 144, 192, 194
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€.
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 railway station.
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.
| Application Deadline: | 2014/09/05 | (expired) |
|---|---|---|
| Notification until: | 2014/09/15 | (expired) |
| Summer School: | 2014/10/27 - 2014/10/31 | (expired) |
