معرفی
Michael Leuschel is a Professor in the Institute of Computer Science at Heinrich-Heine-Universität Düsseldorf, Faculty of Mathematics and Natural Sciences. He leads research in formal methods, programming languages, and software engineering, with a focus on the development and application of the ProB model checker and constraint solver. He is co-founder of Formal Mind and scientific advisor to Nobreach, and actively contributes to the formal methods community through editorial and organizational roles.
His research interests include formal verification, model checking, logic programming, partial evaluation, and the B and Event-B methods. He has pioneered techniques for animating and validating formal models, with applications in safety-critical systems such as railway operations. His work bridges theoretical foundations with industrial practice, enabling rigorous software construction.
The recent publications highlight a strong trend in applying formal methods to AI safety, particularly in railway systems (e.g., KI-LOK project), integrating reinforcement learning with safety shields, and validating AI-based components. Other themes include interactive simulation, domain-specific validation documents, and the use of ProB for TLA+ and railML. The work combines theoretical advances in model checking with practical tool development.
Michael Leuschel has supervised numerous students and collaborators, including Jens Bendisposto, Sebastian Krings, Philipp Körner, and Joshua Schmidt. He has been involved in significant research grants and projects, such as KI-LOK and the development of ProB, often in collaboration with industry and other academic institutions. His work has led to the creation of widely used tools and methodologies in formal methods.
He is a key member of the Software Engineering and Programming Languages research group. His team develops and maintains ProB, works on integrating formal models into applications, and explores new frontiers in AI validation using formal techniques. The group is active in both theoretical research and practical tool building.




