Verification and Static Analysis of Software

Seminar in Theoretical CS, Summer Semester 2017


  • 13.01.2017: we are online


20.04.2017, 13:00 Introduction at seminar room of i2 (building E1, room 4201b)
15.05.2017 Detailed outline of report due
12.06.2017 Seminar report due
03.07.2017 Presentation slides due
17.07.2017, 09:00 Seminar at seminar room of i2 (building E1, room 4201b)


The term verification refers to theory and practice of computer-supported formal analysis methods for ensuring correctness of (hardware and) software systems. The modeling and verification of such systems is an important issue. In particular, safety-critical systems are ones in which errors can be disastrous: loss of life, major financial losses, etc. Techniques to safeguard against such scenarios are essential for such systems. Testing can identify problems, especially if done in a rigorous fashion, but is generally not sufficient to guarantee a satisfactory level of quality.
To ensure the soundness of verification results, formal methods for analysing software on source-code level have been and are being developed, commonly referred to as Static (Program) Analysis.  Related techniques such as data-flow analysis or abstract interpretation have originally been designed for enabling code optimisation or highlighting possible coding errors. Nowadays, they are increasingly being employed for semantics-oriented activities such as proving software correctness.

The goal of this seminar is to give an overview of the related research activities of the MOVES group. It covers several areas of computer science to which computed-aided verification techniques and related analysis methods are central, and which represent the research fields of the respective supervisors. Each area features a number of topics which are described in a scientific journal or conference article. These research articles are the basis on which students have to prepare their report and presentation.


Basic knowledge in the following areas is expected:

  • Formal languages and automata theory
  • Mathematical logic
  • Previous knowledge in semantics of programming languages, program analysis, model checking and/or concurrency theory is helpful but not mandatory


Pointer and Shape Analysis

  1. Fractional Permissions for Concurrency
  2. Symbolic Permission Accounting
  3. Compositional Shape Analysis by means of Bi-Abduction
  4. Amortised Resource Analysis

Advanced Model Checking Techniques

  1. Counterexample-Guided Abstraction Refinement
  2. Assume-Guarantee Reasoning
  3. Fairness
  4. Bounded Model Checking
  5. Configurable Software Verification
  6. IC3
  7. Probabilistic Model Checking
  8. Monte Carlo Model Checking
  9. Concurrent Model Checking Algorithms

Analysis of Probabilistic Programs

  1. Sampling for Probabilistic Programs
  2. Slicing Probabilistic Programs
  3. Sampling Functions for Probability Distributions
  4. Static Analysis of Probabilistic Programs
  5. Probabilistic Termination

Additional Material


Registration to the seminar is handled between January 13 and 29, 2017, via the central online form. Later applications will not be considered.


Thomas Noll <noll at>