Trends in Computer-Aided Verification (Seminar)

Seminar in Theoretical CS, Winter Semester 2015/16


  • 05.11.2015: Topics assigned
  • 22.06.2015: we are online


Wed, 28.10.2015, 16:00 Introduction at room 9U09
30.11.2015 Detailed outline due
11.01.2016 Seminar report due
22.01.2016 Presentation slides due
28./29.01.2016 Seminar at Inf. 2 (room 4201b)


The term Computer-Aided Verification refers to theory and practice of computer-supported formal analysis methods for both 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.
Formal methods, on the other hand, offer techniques ranging from the description of requirements in a formal notation to allow for rigorous reasoning about them, to techniques for automatic verification of software. Due to the complexity of these approaches and the systems they are applied to, automated computer support is indispensable.

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

The following list gives an overview of the areas that will be covered. For getting an overview of possible related topics, we refer to the previous seminar in winter semester 2014/15.

  • Abstraction methods for pointer programs
  • Verification methods for Programmable Logic Controller (PLC) software
  • Semantics and verification of probabilistic systems
  • Formal methods for security analysis


Inductive Verification

  1. Efficient Abstraction Refinement
  2. Efficient Computation of Weakest Preconditions
  3. Property-Directed Inference

Analysis of Dynamic Communication and Data Structures

  1. Analysis of infinite-state graph transformation systems
  2. Analysis of heap structures with data
  3. Analysis of concurrent data structures

Probabilistic and Approximate Computations

  1. Cost-Based Analysis of Probabilistic Programs (English only!)
  2. Relational Hoare Logic for Probabilistic Programs (English only!)
  3. Correctness of Approximate Computations (English only!)

Formal Approaches to Systems Engineering

  1. Formal requirements engineering(English only!)
  2. Contract-based safety assessment (English only!)
  3. Probabilistic safety and liveness (English only!)

Automata, Logics, and Games

  1. The Cyclic-Routing Problem (English only!)
  2. Pareto Curves for probabilistic Model Checking (English only!)
  3. Finite Optimal Control for Time-Bounded Reachability in CTMDPs and Continuous-Time Markov Games (English only!)

Information Flow Analysis for Security

  1. Type-based information flow analysis
  2. Information flow analysis based on program dependence graphs
  3. Model-driven information flow analysis

Formal Methods in System Design

  1. Model checking and performance of shared-memory mutual exclusion protocols
  2. Modelling and Analysis of Markov Automata
  3. Model Checking Linearizability via Refinement

Schedule of Talks

Thursday 28.01.2016
09:00-11:15 7, 8, 13
11:30-13:00 19, 20
14:00-16:15 1, 2, 3
Friday 29.01.2016
09:00-11:15 4, 5, 6
11:30-13:00 11, 12
14:00-16:15 16, 17, 18


Basic knowledge in the following areas is expected:

      • Formal languages and automata theory
      • Mathematical logic
      • Previous knowledge in semantics of programming languages and concurrency theory is helpful but not mandatory


Registration to the seminar is handled between June 25 and July 8, 2015, via the central online form.

Additional Material


Thomas Noll <noll at>