first.last@kcl.ac.uk (PGP Key) Room (N)7.15 Bush House 30 Aldwych London WC2B 4BG
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.
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 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.
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)