Can we model check the world?
My research is about applying formal methods and machine learning in safety-critical systems, e.g., self-driving cars, trains, and aircraft. Machine learning bears the promise of letting machines learn by themselves, given enough training data. However, it has no guarantee of correctness, safety, or security. My research aims to overcome these shortcomings via formal methods as they are based on mathematics and can provide rigorous analysis, such as formal verification.
SATISFIES (Holistic Synthesis and Verification for Safe and Secure Autonomous Vehicles). 2024 - 2026. KKS funded. Industrial partners: Volvo Car, Zenseact, Mimer Information Technology.
Co-editor: Frontiers in Control Engineering - Formal Verification of Neural Networks-Based Control Architecture for Safety-Critical Autonomous Systems. 🎉This research topic is open for articles now! Welcome to submit your work!🎉
Reviewer/sub-reviewer: FM Symposium, AST, NFM, FMICS, SERENE, ISEC, Science of Computer Programming, Journal of Robotics, IEEE Transactions on Intelligent Transportation Systems, Journal of Supercomputing, Journal of Software and Systems Modeling, Journal of Systems & Software, etc.
Organizing conferences/workshops: AEiC 2026 (Industrial track co-chair)(🎉open for submissions now!🎉), IEEE SSE 2024 - present (PC member), SEAA 2024 - present (PC member), ASYDE 2024 - present (PC member), SPIN 2024 (PC member). ECBS 2023 (Tool Demo Chair), MODELS 2023 (Volunteer), ICST 2018 (Volunteer).
Invited seminars/conferences: Dagstuhl Seminar 24071 - Safety Assurance for Autonomous Mobility. FM Symposium 2024 (invited journal first). QUATIC 2023 (invited journal first).
Volvo Car. Volvo Construction Equipment. Zenseact. Mimer Information Technology, Scania.
Catching Bugs by Formal Verification (2018 - 2025)
Development of Web Application (2017 - 2019)
Data Communication (2018 - 2024)
Programming with Python (2022 - 2023)
Guest lecturer of course: DVA482 Embedded Systems II. 2021 - 2025.
Guest lecturer of course: FLA433 Autonomous Vehicle. 2024 - 2025.
Generating Scenarios from Formal Specifications for Autonomous Vehicles. Company info: Scania.
Safe Motion Planning and Reinforcement Learning for Self-Driving Vehicles and Robots.
Supervisor of Bachelor theses.
Model Checked Reinforcement Learning For Multi-Agent Planning. Erik Wetterholm. 2023.
Supervisor of Master theses.
Fine-Tuning LLM for Scenario Generation for ADAS Systems. Ammara Asif. 2025. Company: Volvo Cars.
Integrating the power of large language models and model checking in requirement engineering. Gayomi Patikirige. 2025.
Overcoming the ambiguity and inconsistency of requirements by using generative AI. Ishimwe Kwizera. 2024. Company: Alstom.
Safety-Guaranteed Mission Planner for Autonomous Vehicles. Đorđe Kalezić. 2020.
Co-supervisor of PhD students