Alexandru Mereacre

Alexandru Mereacre is a researcher in the Department of Computer Science at the University of Oxford, where he held the position of Research Assistant until June 2015. His primary research focuses on probabilistic verification, controller synthesis for stochastic hybrid systems, and formal analysis of Markov chains. He completed his PhD at RWTH Aachen University in 2011, titled 'Verification of Continuous-Space Stochastic Systems.'

His work emphasizes quantitative model checking of probabilistic systems, particularly discrete-time and continuous-time Markov chains, and their applications in real-time and hybrid systems. Mereacre has contributed to the development of efficient algorithms for controller synthesis and parameter synthesis in systems such as embedded and medical devices. He has collaborated on projects like VERIWARE and VERIPACE, addressing challenges in automated verification and stochastic modeling.

Key research themes include formal methods for probabilistic systems, timed automata specifications, and energy-efficient scheduling in embedded systems. His publications span topics like battery optimization, cardiac pacemaker parameter synthesis, and verification techniques for hybrid systems.