Bio: I am a lecturer (equiv. to assistant professor) and member of the Reasoning and Planning Group at King's College London. Before that, I was a post-doc in the Chair for Logic and Verification at Technische Universität München. I was awarded my PhD from the Australian National University, and, before that, an MSc from Cairo University. I also held full-time industry R&D positions from 2009 to 2013 in electronics CAD software and FPGA system design.

Research Interests:

• Formalising mathematics in Isabelle/HOL. E.g.
  • Building a formal library on combinatorial optimisation
  • Building a formal library on computation models and complexity theory
  • Formalising variants of Stokes' theorem, e.g. Green's theorem
• Formal verification of AI algorithms and systems. E.g.
  • Building a suite of formally verified tools for model-checking and AI planning
• Algorithms for AI planning and model checking E.g.
  • Algorithms for computing upper bounds on state space diameters
  • Algorithms for reachability that exploit symmetries

Working Papers:

• Proof-Producing Translation of Functional Programs into a Time and Space Reasonable Model
  Kevin Kappelmann, Lukas Stevens, Fabian Huch, and Mohammad Abdulaziz
• A Formal Correctness Proof of Edmonds' Blossom Shrinking Algorithm
  Mohammad Abdulaziz

Book Chapters:

• Graph Algorithms
  Mohammad Abdulaziz
  In Functional Data Structures and Algorithms: A Proof Assistant Approach. Editor: Tobias Nipkow. ACM Books, 2025.

Journal Publications:

• An Isabelle/HOL Formalisation of Green's Theorem
  Mohammad Abdulaziz and Lawrence C Paulson
  Journal of Automated Reasoning, 2019
• Formally Verified Algorithms for Upper Bounding State Space Diameters
  Mohammad Abdulaziz, Michael Norrish, and Charles Gretton
  Journal of Automated Reasoning, 2018

Conference Publications:

• A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
  Bram Kohlen, Maximilian Schäffeler, Mohammad Abzulaziz, Arnd Hartmanns, and Peter Lammich
  In the International Conference on Computer-Aided Verification (CAV), 2025
• Formally Verified Approximate Policy Iteration
  Maximilian Schäffeler and Mohammad Abdulaziz
  In the AAAI Conference on Artificial Intelligence (AAAI), 2025
• Interactive Theorem Provers: Applications in AI, Opportunities, and Challenges
  Mohammad Abdulaziz
  In the AAAI Conference on Artificial Intelligence (AAAI): AAAI-24 Special Track AI for Social Impact, Senior Member Presentations, New Faculty Highlights, Journal Track, 2024
• A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows
  Mohammad Abdulaziz and Thomas Ammer
  In the International Conference on Interactive Theorem Proving (ITP), 2024
• A Formal Analysis of RANKING
  Mohammad Abdulaziz and Christoph Madlener
  In the International Conference on Interactive Theorem Proving (ITP), 2023
• Formally Verified SAT-Based AI Planning
  Mohammad Abdulaziz and Friedrich Kurz
  In the AAAI Conference on Artificial Intelligence (AAAI), 2023
• Formally Verified Solution Methods for Markov Decision Processes
  Maximilian Schäffeler and Mohammad Abdulaziz
  In the AAAI Conference on Artificial Intelligence (AAAI), 2023
• Formal Semantics and Formally Verified Validation for Temporal Planning
  Mohammad Abdulaziz and Lukas Koller
  In the AAAI Conference on Artificial Intelligence (AAAI), 2022
• Computing Plan-Length Bounds Using Lengths of Longest Paths
  Mohammad Abdulaziz and Dominik Berger
  In the AAAI Conference on Artificial Intelligence (AAAI), 2021
• Computing Plan-Length Bounds Using Lengths of Longest Paths (Extended Abstract)
  Mohammad Abdulaziz and Dominik Berger
  In the International Symposium on Combinatorial Search (SoCS), 2020
• Trustworthy Graph Algorithms (Invited Talk)
  Mohammad Abdulaziz, Kurt Mehlhorn, and Tobias Nipkow
  In the International Symposium on Mathematical Foundations of Computer Science (MFCS), 2019
• A Verified Compositional Algorithm for AI Planning
  Mohammad Abdulaziz, Charles Gretton, and Michael Norrish
  In the International Conference on Interactive Theorem Proving (ITP), 2019
• Plan-Length Bounds: Beyond 1-way Dependency
  Mohammad Abdulaziz
  In the AAAI Conference on Artificial Intelligence (AAAI), 2019
• A Formally Verified Validator for Classical Planning Problems and Solutions
  Mohammad Abdulaziz and Peter Lammich
  In the International Conference on Tools in Artificial Intelligence (ICTAI), 2018
• A State Space Acyclicity Property for Exponentially Tighter Plan Length Bounds
  Mohammad Abdulaziz, Charles Gretton, and Michael Norrish
  In the International Conference on Automated Planning and Scheduling (ICAPS), 2017
• An Isabelle/HOL Formalisation of Green's Theorem
  Mohammad Abdulaziz and Lawrence C. Paulson
  In the International Conference on Interactive Theorem Proving (ITP), 2016
• Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems
  Mohammad Abdulaziz, Charles Gretton, and Michael Norrish
  In the International Conference on Interactive Theorem Proving (ITP), 2015
• Exploiting Symmetries by Planning for a Descriptive Quotient
  Mohammad Abdulaziz, Michael Norrish, and Charles Gretton
  In the International Joint Conference on Artificial Intelligence (IJCAI), 2015

Workshop Publications:

• Cost Optimal Planning as Satisfiability
  Mohammad Abdulaziz
  In the Workshop on Heuristics and Search for Domain-Independent Planning, 2021
• Mechanising Theoretical Upper Bounds in Planning
  Mohammad Abdulaziz, Charles Gretton, and Michael Norrish
  In the Workshop on Knowledge Engineering for Planning and Scheduling (KEPS), 2014
• A machine learning technique for hardness estimation of QFBV SMT problems
  Mohammad Abdul Aziz, Amr Wassal, and Nevine Darwish
  In the International Workshop on Satisfiability Modulo Theories (SMT), 2012

Formalisations:

• A formalisation of the semantics of a fragment of PDDL AFP Entry
• A formalisation of a SAT-based planning encoding AFP Entry
• A formalisation of Green's theorem in Isabelle/HOL, and some applications of it AFP Entry
• A formalised theory library for factored transition systems and planning problems in HOL4 Download
• A porting of some of the HOL4 factored system theory in Isabelle/HOL AFP Entry

Software:

• FormPlan: A Formally Verified Planning Toolkit Website
• A program that computes plan length upper bounds for SAS+ planning problems Download
• A planner for SAS+ planning problems which have symmetries Download

Opportunities for students:

• If you want to do a Phd (or a Master Bachelor or a Bachelor) with me, please take a look into these themes and let me know what you find interesting. Then we could come-up with a more concrete topic.

Supervision:

I have been fortunate to work with:

• Thomas Ammer (PhD at KCL, 2023-)
• James Spence (PhD at KCL, 2023-)
• David Wang (PhD at KCL, 2023-)
• Maximilian Schäffeler (PhD at TUM, 2021-, co-supervised with Prof. Tobias Nipkow)

• Shriya Meenakshisundaram: Formalising the Theory and Algorithms for Greedoids (MSc at KCL, 2024)
• Thomas Ammer: Formal Verification of Orlin's Algorithm (MSc at TUM, 2023)
• Christoph Madlener: Formal Primal-Dual Analysis of Online Matching Algorithms (MSc at TUM, 2022)
• Florian Keßler: Formalising the Semantics of Actions with Continuous Change (MSc at TUM, 2022)
• Ralitsa Dordjonova: Linear Programming Characterisations of Matching (MSc at TUM, 2022)
• Florian Sextl: Automating Proofs for Reasoning about Parallel Programs in Isabelle/HOL (MSc at TUM, 2021-2022, co-supervised with Simon Roßkopf and Fabian Huch)
• Maximilian Schäfeler: Formal Verification of Solution Methods for MDPs (MSc at TUM, 2021)
• Friedrich Kurz: Formally Verified SAT Encoding of Planning (MSc at TUM, 2019)

• Nathan Lutala: Formally Verified Quad-Trees (BSc at KCL, 2024)
• Salama Khan: Bounding State-Space Diameters in Planning Problems (BSc at KCL, 2024)
• Johannes Neubrand: Automated Refinement of Functional Programs to Imperative Programs (BSc at TUM, 2022-2023)
• Alexander Schlenga: Upper-Bounding Transition System Diameters Using QBF (BSc at TUM, 2021)
• Bilel Ghorbel: Refining Functional Programs to Deeply Embedded Imperative Programs (BSc at TUM, 2021)
• Lukas Koller: Formalisation of the Semantics of Temporal Planning (BSc at TUM, 2021)
• Malek Souissi: SMT-Based Optimal AI Planning (BSc at TUM, 2020)
• Dominik Berger: Computing Upper Bounds on Plan Lengths (BSc at TUM, 2019)