Trends in Computer-Aided Verification (Seminar)

Seminar in Theoretical CS, Winter Semester 2014/15


  • 30.06.2014: we are online


15.10.2014, 15:00 Introduction at seminar room of i2
-8 weeks Table of contents due
-6 weeks Preliminary version of report due
-4 weeks Final version of report due
-2 weeks Preliminary version of slides due
-1 week Final version of slides due


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 system 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 (please refer to the references below). 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 and concurrency theory is helpful but not mandatory


(all presentations as “double features” on Thursdays 08:30-10:00 at I2 seminar room)

Axiomatic Verification

  1. Permission Accounting in Separation Logic
  2. Hoare-Style Verification of Graph Programs
  3. Implicit Dynamic Frames

Graph-Based Abstraction

  1. Grammar-Based Shape Analysis
  2. Abstraction by Hyperedge Replacement Grammars

Inductive Incremental Verification

  1. Software Model Checking via IC3
  2. IC3 Modulo Theories via Implicit Predicate Abstraction

Verification of Probabilistic Systems

  1. Assume-Guarantee Reasoning
  2. Analysis of Markov Decision Processes

Additional Material


Registration to the seminar is handled between July 4 and 20, 2014, via the central online form.


Thomas Noll <noll at>