Welcome to the 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 (such as correctness, safety, reliability, performance and survivability) of software systems 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 (generalised) stochastic Petri nets.
• TODO

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), the DFG Research Training Group UnRAVeL, the German Research Council (DFG), the Dutch Research Council (NWO and STW), 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).

Latest News