I am a PhD student in Tobias Nipkow's group at the Technical University of Munich. My research interests evolve around algorithm verification with Isabelle/HOL and model checking of (probabilistic) timed automata.
I am constructing a model checker for the popular realtime-systems model formalism of timed automata. The clou is that the model checker's correctness is formally proved in Isabelle/HOL. For more information see our paper and the Github repository.
We (Shuwei Hu, Tobias Nipkow, and me) are constructing a verified tool in Isabelle/HOL for the automatic memoization of verified functional programs. The functional programs can be used to describe dynamic programming algorithms. The memoization can target functional and imperative code. For more information see our paper and the AFP entry.
We (Fabio Madge Pimentel and me) are working on the core resolution primitive in Isabelle's logical inference kernel. Its been around in its current form since the early days of Isabelle and still needs to trust an implementation of a complex higher-order unification algorithm due to Huet. Our goal is to instead certify unifiers for higher-order terms in the kernel, and to thus move the unification algorithm out of the trusted code base. Furthermore, we hope to facilitate experimentation with unification in Isabelle once the unification results do not have to be trusted anymore. For further information see my workshop paper.