Welcome to the Chair for Software Modeling and Verification!

The Software Modeling and Verification Group (MOVES), headed by Prof. Dr. Ir. Dr. h. c. Joost-Pieter Katoen, is one of the research units in the Department of Computer Science. Our research and teaching program is concerned with the study, development and application of formal methods to software design in a broad sense. Our activities concentrate on modeling and verifying trustworthiness aspects (such as safety, reliability, performance and survivability) of software systems by applying mathematical theories and methods.

Major research topics of interest are:

  • modeling formalisms for concurrent systems
    (such as process algebras, statecharts, message sequence charts and mobile process calculi);
  • model checking and quantitative extensions thereof
    (in particular probabilistic model checking, cost bounds, abstractions, counterexample generation);
  • semantics and analysis of modern programming languages
    (among others, semantics of Erlang, heap abstractions and pointer analysis, multi-threading, loop-invariant synthesis, probabilistic programming);
  • probabilistic models for concurrency
    (i.e., the theory of models, abstraction, refinement, continuous-time stochastic models with nondeterminism, new analysis techniques, etc.).

Our research is conducted in the context of several projects (such as ATTESTOR, CEBUG, ROCKS, SYRUP) that are funded by the Dutch Research Council (NWO), the German Research Council (DFG), the European Union (CARP, D-MILS, MEALS, MoVeS and SENSATION), and the European Space Agency (CATSY, COMPASS 3.0). The MOVES group is responsible for and participates in the DFG Research Training Group UnRAVeL.

Our theoretical research is largely tool- and application-oriented. Tools such as storm (symbolic and explicit-state probabilistic model checker), Prophesy (parameter synthesis), Prinsys (invariant synthesis), libalf (automata learning tool), MRMC (probabilistic model checker), IMCA (real-time stochastic games), Smyle (analysis and synthesis of message sequence charts), and Juggrnaut (pointer program analyzer) have been developed in this group.

The MOVES Group hosts www.etaps.org.