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, where I am still a guest researcher and a regular visitor. 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.
Formalising mathematics in Isabelle/HOL. E.g.
Matching algorithms, like Edmonds' Blossom Algorithm and the Micali-Vazirani algorithm for maximum matching.
Graph algorithms, like approximating graph eccentricities.
Different variants of Stokes' theorem.
Modelling computation and complexity theory, like the Cook-Levin theorem.
Formal verification of AI algorithms and systems using interactive theorem provers. E.g.
A formally verified SAT-based planner in Isabelle/HOL.
Formalised the semantics of PDDL in Isabelle/HOL, and building a plan validator based on that.
Verification of diameter upper bounding and symmetry breaking algorithms in HOL4.
Algorithms for classical AI planning and graph theoretic problems defined on state spaces. E.g.
Computing upper bounds on state space diameters.
Exploiting symmetries for more effective reachability algorithms.
Two fully funded projects ( project 1 and project 2) with the UKRI Centre for Doctoral Training on Safe and Trusted AI, which is a joint centre between King's College London and Imperial College London. If you would like to work on either project please contact me and consider applying.
There is a fully-funded PhD that is not tied to a specific topic. Please contact me if you want to apply to that. I expect you to have taken a look into my publications and these project themes, and to have made-up your mind as to what themes you find interesting. Then we could come-up with a more concrete topic.
If you are in London or in Munich, and want to do a Bachelor or a Master thesis 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.
I have been fortunate to work with:
Maximilian Schäffeler: Verified Solution Methods for MDPs (PhD at TUM, 2021-, informally co-supervised with Prof. Tobias Nipkow)
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)
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)