Modeling and analysis of safety, dependability, performance, and security aspects of
software-intensive embedded systems by means of model checking, automated planning,
theorem proving and testing.
Synthesis of parameters and strategies, schedules and plans,
for the control and testing of safety-critical systems.
The development of new model checking techniques based on symbolic techniques
(e.g. abstraction, confluence, fixpoint equation systems, constraint solving) and
high-performance graph algorithms (e.g. distributed and multi-core model checking algorithms).
include embedded systems (e.g. railway safety interlockings), distributed systems (e.g. blockchain and smart contracts),
security protocols and risk analysis (e.g. through attack-defense trees),
energy optimisation (e.g. through stochastic timed automata)
and signaling pathways in biological systems.