
معرفی
Mohammad Abdulaziz Mansour is a Lecturer in Artificial Intelligence at King's College London, affiliated with the Department of Informatics within the Faculty of Natural, Mathematical & Engineering Sciences. Previously, he held a post-doctoral researcher position at the Chair for Logic and Verification at TU München and remains a visiting researcher there. His work focuses on formal methods, theorem proving, and their applications in AI, particularly in algorithm verification, planning, and graph theory.
Research Interests: Formal verification of AI algorithms, formalization of mathematics, graph algorithms, Markov Decision Processes, and SAT-based planning. His contributions emphasize rigorous validation through proof assistants like Isabelle/HOL, ensuring correctness of algorithms in critical domains such as cybersecurity and automated reasoning.
Publications highlight his expertise in formal analysis of algorithms (e.g., matroids, minimum cost flows) and verified solutions for MDPs. He collaborates with institutions like the King's Cybersecurity Centre, contributing to research themes in reasoning, planning, and software systems security.
Recent work includes advancements in formally verified approximate policy iteration and formally validated SAT-based AI planning methods. His research bridges theoretical computer science with practical applications, ensuring foundational algorithms are both efficient and correct.





