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.
• Caesar, a deductive verifier for randomised algorithms, implemented in Rust. It encodes a program and specification in an intermediate verification language (IVL). This IVL is relatively complete and features quantitative generalisations of assume- and assert statements. Its modular set-up enables to (i) prototype and automate new verification techniques, (ii) combine proof rules, and (iii) benefit from back-end improvements. It uses modern SMT solvers as back-end.
• Using in-house developed, scalable parameter synthesis techniques, supported by our tool Prophesy, we have automatically synthesised the optimal bias of randomisation in Herman’s ring protocol, a prominent self-stabilising 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 standardisation process.
• 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. We developed NITWIT, an independent tool to verify violation witnesses of software model checkers.
• 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 randomised algorithms, exact inference in probabilistic programs, and — by extending separation logic — proving properties of randomised algorithms manipulating 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), 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).