Summer School 2012: Verification Technology, Systems & Applications

VTSA08

The summer school on verification technology, systems & applications takes place at Max Planck Institute for Informatics at Saarbrücken, Germany, from September 03th-07th. 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 Armin Biere, Ahmed Bouajjani, Jürgen Giesl, David Monniaux, Carsten Schürmann 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, accomodation and daily living costs on their own. Recommendations on hotels can be found below.

Application

Please apply electronically by sending an email to Manuel Lamotte-Schubert (lamotte (at) mpi-inf.mpg.de) including

until the 20th of July, 2012.. Notifications on acceptance will be given by 3th of August, 2012.

Registration

The registration will be open to accepted applicants starting on 3th of August, 2012.

Program

All lectures will take place in room 024 at the ground floor of the Max Planck Institute for Informatics (MPI-INF, building E1 4) located on the university campus of Saarbrücken.

Schedule

September 03
Monday
September 04
Tuesday
September 05
Wednesday
September 06
Thursday
September 07
Friday
9.00-12.30 Carsten Schürmann
Slides Part 1
Armin Biere
All Slides
David Monniaux
All Slides
Ahmed Bouajjani
Slides Part 1 | Part 2
Jürgen Giesl
Slides Part 2
12.30-14.00 Lunch break
14.00-17.20 Armin Biere
All Slides
Carsten Schürmann
Slides Part 2
Jürgen Giesl
Slides Part 1
David Monniaux
All Slides
Ahmed Bouajjani
Slides Part 3 | Part 4
17.30-18.30 Student sessions:
  • Alexander Weinert
    (RWTH Aachen)
    Slides
  • Markus Normann Rabe
    (Saarland University)
  • Martin Suda
    (MPI-INF)
    Slides
Student sessions:
  • David Hauzar
    (Charles University)
  • András Vörös
    (BME MIT FTSRG, Hungary)
  • Reiner Hüchting
    (TU Kaiserslautern)
  • Tom van Dijk
    (University of Twente)
Student sessions:
  • Andrei Dan
    (ETH Zurich)
    Slides
  • Klaas Boesche
    (Saarland University)
  • Babak Bagheri
    (KRDB Research Centre,
    Free University of Bozen)
    Slides
  • Alexander Bau
    (HTWK Leipzig)
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 with world leading experts in a relaxing atmosphere.

Lecturer(s)

Armin Biere
Armin Biere

Understanding Modern SAT Solvers

SAT solving techniques are used in many automated reasoning engines. This lecture starts with basic techniques for SAT solving and then continues discussing more recent developments for practical SAT solving. This includes improvements of the basic conflict driven clause learning (CDCL) algorithm, as well as advanced preprocessing respectively inprocessing techniques. The lecture concludes with a brief overview on current trends in parallelizing SAT.

Jürgen Giesl
Jürgen Giesl

Automated Termination Analysis

Termination is a crucial property of programs. Therefore, techniques to analyze the termination behavior automatically are highly important for program verification. Traditionally, techniques for automated termination analysis were mainly studied for declarative programming paradigms such as logic programming and term rewriting. However, in the last years, several powerful techniques and tools have been developed which analyze the termination of programs in many programming languages including Java, C, Haskell, and Prolog.
In the tutorial, we give an overview on techniques for automated termination analysis of several different programming languages. We start with the foundations of termination proving and introduce powerful techniques to analyze declarative programming paradigms like term rewriting. Afterwards, we show how to extend such techniques in order to tackle programs in real imperative, functional, or logic programming languages. To this end, we present automated termination techniques for Java, Haskell, and Prolog. While most approaches in the area try to prove termination, we also discuss methods to disprove termination, which is crucial for debugging programs. Moreover, we show that termination techniques can also be applied for automated complexity analysis. In this way, one can use the information obtained from termination proofs in order to derive upper bounds on the runtimes of programs automatically.

David Monniaux
David Monniaux

Abstract Interpretation

Reasoning over programs generally involves obtaining invariants, that is, properties that are valid at every program step (or at every loop iteration, or for any recursive call to a function...). Most programs are effectively infinite state systems (even if their state space is finite, it is so large that it should be treated as infinite), thus methods based on finding strongest invariants (exact reachable states) generally fail. Abstract interpretation finds inductive invariants within a suitably selected abstract domain (e.g., for numerical variables, intervals of variation). This restriction allows for efficient techniques for finding invariants. The course will cover basic concepts (abstract domains, correctness, Kleene iterations), industrial aspects (analysis in the large), and instances of more advanced techniques (predicate abstraction, integration with SAT or SMT solvers, etc.).

Ahmed Bouajjani
Ahmed Bouajjani

Verification of Concurrent Programs under Weak Memory Models

The course starts with an introduction of basic notions and techniques for the verification of infinite-state systems, and an overview of recent results on algorithmic verification of concurrent programs. Then, the rest of the course is devoted to the problem of verifying concurrent programs running under weak memory models. For performance reasons, modern multiprocessors and compilers relax the program order between actions, i.e., they may reorder actions issued by a same processor/thread, and therefore, computations are not necessarily sequentially consistent (SC). We address the questions of (1) checking reachability problems under weak memory models, and (2) checking robustness of a program against a weak memory model, i.e., whether all the visible behaviors of the program under that memory model are also possible under the sequential consistency model.

Carsten Schürmann
Carsten Schürmann

Logical Frameworks - The Art of Representation

Representation and reasoning are the two defining properties of mechanized mathematics. Representing a problem well often yields simple and easy understandable proofs. The more convoluted the representation the more lemmas become necessary. In this course we will focus on one such representation language, a logical framework that is based on linear logic, discuss its philosophical foundations, illustrate its application by examples, and experiment with its implementation: the Celf system.

Accommodation

The participants are responsible for their room reservations.
We have reserved rooms at a special rate in the following hotels. Please book the rooms yourself using the keyword "MPI".

Another hotel recommendation is Motel One Saabrücken for which we could not reserve rooms in advance. Therefore, please ask yourself to make a booking.

Arrival / Directions

The Summer School 2012 will take place at the campus of Saarland University, in the building of the Max Planck Institute for Informatics (MPI-INF), building E1 4) located on the university campus. For more information on Saarbrücken, you can also check here and here.

Travelling to Saarbrücken

General instructions: Directions

With Public Transportation from the City to the MPI-INF

Please use the connection planning tool offered by the public transportation in Saarland:

By Car

Please use the multi-storey car park "Uni-Ost". Pull a parking ticket. On departure you will get a free ticket for leaving the car park.


General Locations and Tips

There are lots of cozy little pubs and cafés in Saarbrücken, for example:

Organization and Contact

General Organization

Local Organization

Website

For comments or questions send an email to Jennifer Müller (jmueller(at) mpi-inf.mpg.de).

The summer school is organized by the Montefiore Institute, University of Luxembourg, INRIA Nancy, and the Max Planck Insitute for Informatics Saarbrücken.

Important Dates

(Format is MM/DD/YYYY)

Photos

Photos of the event can be found here.

Sponsored by
INRIA MPII University of Lige Luxembourg
fnrs Moves SNT