Current third-party funded projects:

QuantLA

DFG Research Training Group "Quantitative Logics and Automata"

HAEC

Collaborative Research Centre SFB912 "Highly Adaptive Energy-Efficient Computing"

QuaOS

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.

SYANCO

bilateral DFG-NWO project "Synthesis and analysis of component connectors"

ProbPor II

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).

ROCKS

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:

PROCOPE

DAAD project PROCOPE: academic research collaboration with Dr. Nathalie Bertrand (France)

PROALAR

DAAD project PROALAR: academic research collaboration with Prof. Dr. Pedro D'Argenio (Argentina) (together with Prof. Dr. Holger Hermanns (Universität Saarbrücken))

CREDO

European Union project "Modeling and analysis of evolutionary structures for distributed services"

ProbPor

DFG-project "Reduktionsmethoden zur Verifikation omega-regulärer und temporallogischer Eigenschaften für kommunizierende probabilistische Prozesse": see ProbPor II

VOSS I und VOSS 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.

Veriam

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.

---

Tools:

LTL2DSTAR

a tool hat converts formulas in linear time logic to deterministic omega-automata, specifically Rabin and Streett automata

LiQuor

a tool for model checking Markov decision processes against linear-time specifications

Reo Model Checking Tools

Component based model checking

JINC

an efficient, easy to use and easily expandable BDD package