Current third-party funded projects:
DFG Research Training Group "Quantitative Logics and Automata"
Collaborative Research Centre SFB912 "Highly Adaptive Energy-Efficient Computing"
The scientific goal of the DFG-project QuaOS is research on methods and models that support the quantitative and functional analysis of properties of Mircokernels.
bilateral DFG-NWO project "Synthesis and analysis of component connectors"
One main goal of the DFG project "Reduktionsmethoden zur Verifikation omega-regulärer und temporallogischer Eigenschaften für kommunizierende probabilistische Prozesse II" is the implementation of the model checking tool LiQuor
, which is designed for the analysis of reactive probabilistic systems against omega-regular linear-time specifications. Within this scope, research is also done on various theoretical foundations. Amongst others, a probabilistic variant of partial order reduction has been established and the minimization of automata for linear-time specifications has been investigated (see LTL2DSTAR
The bilateral DFG/NWO project "Rigorous Dependability Analysis using Model Checking Techniques for Stochastic Systems" focuses on modelling and analysis techniques for large scale homogeneous and safety-critical heterogeneous systems.
Former third-party funded projects:
DAAD project PROCOPE: academic research collaboration with Dr. Nathalie Bertrand (France)
DAAD project PROALAR: academic research collaboration with Prof. Dr. Pedro D'Argenio (Argentina) (together with Prof. Dr. Holger Hermanns (Universität Saarbrücken))
European Union project "Modeling and analysis of evolutionary structures for distributed services"
DFG-project "Reduktionsmethoden zur Verifikation omega-regulärer und temporallogischer Eigenschaften für kommunizierende probabilistische Prozesse": see ProbPor II
The bilateral DFG/NWO-projects "Validation of Stochastic Systems I/II" aimed at the integration of modelling and computer-aided verification techniques for the analysis of complex systems with stochastic behaviour. Within the scope of the projects some prominent modelling and analysis techniques have been adapted and extended to a probabilistic setting and several new methods have been developed.
DFG-project "Computerunterstützte Verifikation mit abstrakten Modellen"
DFG-Projekt MA 794/2-1 (und 2-2)
The topic of this project was action refinement in models of reactive systems.
DFG-Projekt MA 794/3-1 (und 3-2)
The topics of this project were specification formalism and the design of verification methods for probabilistic reactive systems.
a tool hat converts formulas in linear time logic to deterministic omega-automata, specifically Rabin and Streett automata
a tool for model checking Markov decision processes against linear-time specifications
Component based model checking
an efficient, easy to use and easily expandable BDD package