Université de Liège

Université de Liège

Université du Luxembourg

Université du Luxembourg

Inria

Inria

Max-Planck-Institut für Informatik

Max-Planck-Institut für Informatik

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.

Application

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

Registration

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.

Program

All lectures will take place in room B001 in Weicker Building of SnT.

Schedule

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

Lecturer(s)

Nikolaj Bjorner
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
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
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
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?
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.
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.
Helmut Veith
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.

Accommodation

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

  1. fill this form (with Adobe Reader or equivalent pdf viewer you can fill the form digitally),
  2. print it,
  3. sign it and
  4. 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:

Weicker building

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

Access

Bus

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

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

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.

Organization and Contact

General Organization

Local Organization

Website

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.

Important Dates

Application Deadline: 2014/09/05 (expired)
Notification until: 2014/09/15 (expired)
Summer School: 2014/10/27 - 2014/10/31 (expired)
(Format is YYYY/MM/DD)

Poster

Sponsored by

Université du Luxembourg

Interdisciplinary Centre for Security, Reliability and Trust

Fonds National de la Recherche

Inria

Max-Planck-Institut für Informatik

Université de Liège

Fonds National de la Recherche Scientifique