The Software Modeling and Verification Group (MOVES), headed by Prof. Dr. Ir. Joost-Pieter Katoen, is one of the research units in the Department of Computer Science.  The research and teaching program of the group is concerned with the study, development and application of formal methods to software design in a broad sense. Current 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, scheduling generation and analysis);
• semantics and analysis of modern programming languages
  (among others, semantics of Erlang, heap abstractions and pointer analysis, multi-threading);
• probabilistic models for concurrency
  (i.e., the theory of models, abstraction, refinement, continuous-time stochastic models with nondeterminism etc.);
• testing and run-time verification (with a focus on real-time issues).

Our research is conducted in the context of several projects that are funded by the Dutch Research Council (NWO), the German Research Council (DFG),  the European Union (Quasimodo, see Info Flyer) , and the European Space Agency (COMPASS).  The MOVES group also participates in the Research Training Group AlgoSyn and the UMIC Cluster of Excellence.   Our theoretical research is largely tool- and application-oriented.

Tools such as MOTOR (process algebra tool), MRMC (probabilistic model checker), Smyle (analysis and synthesis tool for message sequence charts), and TRUTH (model checker) have been developed in this group.

 

The MOVES Group hosts www.etaps.org.