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.