New URL

You have come to an old website. Our new URL is moves.rwth-aachen.de Please update your bookmarks!


Welcome to the Chair for Software Modeling and Verification!

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.  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 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 (such as CEBUG, ROCKS, SYRUP) that are funded by the Dutch Research Council (NWO), the German Research Council (DFG),  the European Union (CARP, MEALSMoVeS and Quasimodo), 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 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.


The MOVES group has been responsible for the local organisation of the co-located conferences  CONCUR 2011, QEST 2011, and TGC 2011, which took place in the week of September 5, 2011 in Aachen.




 

Prof. Dr. Jürgen Giesl  is head of the Teaching and Research Area Informatik 2.