Project themes for prospective students:

If you are interested in doing a project with me (PhD, master's, bachelor's, guided research), take a look into the following general themes, or take a look into the chair for logic and verification website. This should give an idea of what I find interesting.

• 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. results from complexity theory.
• 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.