Bio: I am a senior lecturer (equiv. to associate 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 | Publications | Formalisations | Software | Funding | Teaching | Supervision

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
• Neuro-symbolic AI for mathematics. E.g.
  • AI agents and copilots for interactive theorem proving in Isabelle

Publications (with links to preprints):

Working Papers:

• Testing the Verifier: Automated Testing for Isabelle
  Enzo Bestetti, Bartosz Głowacki, Aravinth Kaneshalingam, Jiangjing Xu, Mohammad Abdulaziz, and Karine Even-Mendoza
• Proof-Producing Translation of Functional Programs into a Time and Space Reasonable Model
  Kevin Kappelmann, Fabian Huch, Lukas Stevens, and 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:

• Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints
  Kevin Kappelmann, Maximilian Schäffeler, Lukas Stevens, Mohammad Abdulaziz, Andrei Popescu, and Dmitriy Traytel
  Lawrence Paulson's 70th Birthday Festschrift, 2026
• A Formal Correctness Proof of Edmonds' Blossom Shrinking Algorithm
  Mohammad Abdulaziz and Kurt Mehlhorn
  Journal of Automated Reasoning, 2026
• 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:

• Formal Primal-Dual Algorithm Analysis (Short Paper)
  Mohammad Abdulaziz, Thomas Ammer, and Christoph Madlener
  In the International Conference on Interactive Theorem Proving (ITP), 2026
• A Formal Analysis of Algorithms for Matroids and Greedoids
  Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, and Adem Rimpapa
  In the International Conference on Interactive Theorem Proving (ITP), 2025
• A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
  Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, 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 Infinite-Horizon 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:

• Formally Verified Certification of Unsolvability of Temporal Planning Problems
  David Wang and Mohammad Abdulaziz
  In KRPlan: Knowledge Representation Meets Automated Planning, 2025
• Mechanically Proving Guarantees of Generalized Heuristics: First Results and Ongoing Work
  Mohammad Abdulaziz, Florian Pommerening, and Augusto B. Correa
  In the Workshop on Heuristics and Search for Domain-Independent Planning (HSDIP), 2022
• Cost Optimal Planning as Satisfiability
  Mohammad Abdulaziz
  In the Workshop on Heuristics and Search for Domain-Independent Planning (HSDIP), 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:

• Isabelle-Graph-Library: A Formal Mathematical Library of Results in Combinatorial Optimisation GitHub
• Archive of Formal Proofs (9 entries):
  • Type Annotations with Roundtrip Property (2026) AFP Entry
  • Nominal Unification (2026) AFP Entry
  • Elementary Graph Traversal Algorithms (2025) AFP Entry
  • Markov Decision Processes with Rewards (2021) AFP Entry
  • Verified Algorithms for Solving Markov Decision Processes (2021) AFP Entry
  • Verified SAT-Based AI Planning (2020) AFP Entry
  • AI Planning Languages Semantics (2020) AFP Entry
  • Upper Bounding Diameters of State Spaces of Factored Transition Systems (2018) AFP Entry
  • An Isabelle/HOL Formalisation of Green's Theorem (2018) AFP Entry
• A formalised theory library for factored transition systems and planning problems in HOL4 Download

Software:

• Isabelle-Graph-Library: A Formal Mathematical Library of Results in Combinatorial Optimisation GitHub
• 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

Funding:

• Copilots for Isabelle: Learning Logical Structure for a Better Proving Experience (2025)
  Scheme: AI for Math by Renaissance Philanthropy (Role: PI at King's College London, co-I's: Andrei Popescu and Dmitriy Traytel)
• Formal Verification of Practical Nominal Unification Algorithms (2025)
  Scheme: Royal Society International Exchange (Role: PI, co-I: Maribel Fernandez)

Teaching:

• Computer-Assisted Theorem Proving (KCL, 2026-)
• Foundations of Computational Theory (KCL, 2025-)
• Machine Learning (KCL, 2025)
• Formal Verification using Interactive Theorem Provers (KCL, 2022-2024)
• Seminar: Formal Verification of Neural Networks (TUM, 2021-2022)
• Functional Data Structures (TUM, 2019-2020)
• Seminar: AI Planning (TUM, 2017-2019)
• Mathematical Logic (TUM, 2018)
• Logic (ANU, 2015)
• Discrete Time Signal Processing (AUC, 2011-2012)

Supervision:

I have been fortunate to work with:

• Maximilian Schäffeler (Post-Doc at KCL, 2026-)

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

• Maximilian Vollath: Formally Verified Grounding Algorithms for AI Planning (MSc at TUM, 2025)
• Shriya Meenakshisundaram: Formalising the Theory and Algorithms for Greedoids (MSc at KCL, 2024)
• Thomas Ammer: Formal Verification of Orlin's Algorithm for Minimum Cost Flows (MSc at TUM, 2023)
• Christoph Madlener: Formal Primal-Dual Analysis of Online Matching Algorithms (MSc at TUM, 2023)
• 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äffeler: Formal Verification of Solution Methods for MDPs (MSc at TUM, 2021)
• Friedrich Kurz: Formally Verified SAT Encoding of Planning (MSc at TUM, 2019)

• Salama Khan: Upper Bounding State Space Diameters (BSc at KCL, 2024)
• Nathan Lutala: Formal Verification of Quadtrees (BSc at KCL, 2024)
• Johannes Neubrand: Refining Programs from HOL to a Deeply Embedded Imperative Language (BSc at TUM, 2023)
• Adem Rimpapa: Formally Verified Certification of the Simplex Algorithm (BSc at TUM, 2022)
• 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)