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).
Application domains
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.
Invited Speaker at
CONCUR 2019, Concurrency Theory, Amsterdam, The Netherlands
Best Student Paper Award at BPM 2018, Sydney Australia, with
Vincent Bloemen, et al.
Best Paper Award at SPIN 2017, Santa Barbara, USA, with Wytse
Oortwijn, et al.
Academic Service (since 2014)
Editorial board SCP
(Science of Computer Programming)
Editorial board STTT
(Software Tools and Technology Transfer)
Member of the Steering Committee SPIN Symposium on Model Checking Software
Member (Chair 2018-2022) of the Steering Committee of FMICS,
the ERCIM working group on Formal Methods in Industrial Critical Systems
PC co-chair of
appFM 2021, 1st IW on Applicable Formal Methods (Beijing, China), with Mario Gleirscher and Jim Woodcock.
Proceedings available as: EPTCS 349
