RWTH Aachen University

MOVES

Software Modeling and Verification

Activate the diagram to roll a six-sided die using fair coin flips. Rapid activations gradually launch larger batches of independent rolls, with up to eight rolls per activation. Hold the diagram or the Enter or Space key for half a second to start or pause automatic rolls. The bars compare how often each face has been rolled.No rolls completed yet.

We are a research group in the Department of Computer Science at RWTH Aachen University. We study formal methods for software systems and develop tools for automated verification.

News

  1. Paper in Theoretical Computer Science

  2. EATCS Best Paper Award

  3. CAV 2027 in Amsterdam

All news
Joost-Pieter
KatoenThomas
Noll
People

Research areas

  • Probabilistic model checking
  • Probabilistic programming
  • Program analysis and verification
  • Semantics and concurrency
Research

Teaching

Research tools

Storm Model checking for probabilistic systems.Caesar Deductive verification of probabilistic programs.
More tools

Research examples

Research

Probabilistic program analysis

We develop weakest precondition calculi for expected runtime analysis of randomised algorithms and exact inference in probabilistic programs. Extensions of separation logic support reasoning about randomised algorithms that manipulate dynamic data structures.

Parameter synthesis

Our tool Prophesy supports parameter synthesis for probabilistic models. Using these techniques, we have synthesised the optimal randomisation bias in Herman’s ring protocol, a self-stabilising distributed algorithm.

Dynamic data structures

Attestor verifies Java programs operating on dynamic data structures. It checks shape and correctness properties, supports reasoning about individual procedures, and provides visual feedback when properties are violated.

C-program verification

In industrial collaborations, we have developed software model checking for C programs in automation and verified automotive software components. Our tool NITWIT independently checks violation witnesses produced by software model checkers.

Safety-critical systems

COMPASS is a toolset for extended AADL, developed with FBK Trento and support from the European Space Agency. It applies formal verification to aerospace systems and has been evaluated on industrial case studies.

Earlier tools

The group has also developed Prinsys (invariant synthesis for probabilistic programs), libalf (automata learning), MRMC (probabilistic model checking), Smyle (message sequence charts), and Juggrnaut (a predecessor of Attestor).