Chair for Software Modeling and Verification
The Software Modeling and Verification Group (MOVES), headed by Joost-Pieter Katoen, is a research unit in the Department of Computer Science at RWTH Aachen University.
We study, develop, and apply formal methods to software systems. This includes applications in cyber-physical systems, safety-critical systems, robotics, and distributed systems.
Our primary focus is on modeling and verifying trustworthiness aspects of software systems – such as correctness, safety, reliability, performance and survivability – by applying mathematical theories and methods. A strong emphasis is on developing software tools that automate the formal verification.
Some recent examples of our research:
- Storm, a symbolic and explicit-state probabilistic model checker. Its main features are: it is modular, has a Python interface enabling rapid prototyping, and — as witnessed by the latest tool competition — is extremely fast. It natively supports among others dynamic fault trees and (generalized) stochastic Petri nets.
- Together with a major stakeholder in automation, we have developed a software model checker for C programs. In cooperation with a major car manufacturer, we formally verified C code of key components in cars.
- Using in-house developed, scalable parameter synthesis techniques, supported by our tool Prophesy, we have automatically synthezised the optimal bias of randomization in Herman’s ring protocol, a prominent self-stabilizing distributed algorithm.
- Supported by several research grants from the European Space Agency (ESA), we have together with FBK Trento developed the comprehensive tool-set COMPASS for extended AADL. This is one of the largest industrial settings using probabilistic model checking. The tool has been validated on industrial case studies by various aerospace companies and our work has influenced the AADL standardization process.
- Attestor, a tool for verifying Java programs operating on dynamic data structures. It features automated verification of shape and correctness properties, supports procedure-modular reasoning, and gives visual feedback in the case of property violations.
- Dijkstra-like weakest precondition calculi for expected run-time analysis of randomized algorithms, for reasoning about conditioning in probabilistic programs and Bayesian networks, and — by extending separation logic — for proving properties of randomized algorithms that manipulate dynamic data structures.
To enable all this, we pursue foundational research in concurrency theory, model checking, probabilistic computation, program analysis, and formal semantics.
Our research is supported by the Advanced Grant project FRAPPANT of the European Research Council, ERC for short, the DFG Research Training Group UnRAVeL, the German Research Council, or DFG for short, the Dutch Research Council, NWO for short, the European Union, the European Space Agency, and various industrial companies.
Earlier software tools developed by our group include: Prinsys (the first loop-invariant synthesis tool for probabilistic programs), libalf (the first tool supporting an extensive set of automata learning algorithms), MRMC (a probabilistic model checker), Smyle (analysis and synthesis of message sequence charts), and Juggrnaut (predecessor of Attestor).