I am a post-doc in the Chair for Logic and Verification at Techniche Universität München. I was awarded my PhD in 2018 from the Australian National University, and, before that, an MSc and a BSc infrom Cairo University in 2009 and 2013, respectively. I also held full-time industry R&D positions from 2009 to 2013 in electronics CAD software and FPGA system design.
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.
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.
If you are interested in doing a project (bachelor's, master's, guided research, praktikum), take a look into the following general themes, or take a look into our chair's website.
Verifying and/or developing logic-based AI algorithms: you could verify existing algorithms for classical planning or planning under uncertainty. Also, you could work on new ideas which improve the state-of-the-art of SAT-based AI planning.
Verifying optimisation or graph algorithms: this includes both algorithms which need substantial (graph) theory to verify, and those needing efficient implementations and data structures. E.g. matching theory, randomised approximation algorithms, etc.
Formalising classical results in theoretical computer science: e.g. PCP theorem.
Applications of Green's theorem or formalising Stokes' theorem: currently, we have in Isabelle a fairly general statement of Green's theorem (i.e. Stokes' theorem on the plane). Project ideas include: interesting (algorithmic) applications of Green's theorem, e.g. handling boundary conditions for interesting PDE's, or formalising theory needed to realise Stokes' theorem, e.g. formalising differential forms and exterior derivatives.