• Alexander Weinert
  (RWTH Aachen)
  Slides
• Markus Normann Rabe
  (Saarland University)
• Martin Suda
  (MPI-INF)
  Slides

• David Hauzar
  (Charles University)
• András Vörös
  (BME MIT FTSRG, Hungary)
• Reiner Hüchting
  (TU Kaiserslautern)
• Tom van Dijk
  (University of Twente)

• Andrei Dan
  (ETH Zurich)
  Slides
• Klaas Boesche
  (Saarland University)
• Babak Bagheri
  (KRDB Research Centre,
  Free University of Bozen)
  Slides
• Alexander Bau
  (HTWK Leipzig)

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.

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.

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

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.

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.