Research Interests

My main interest lies in mathematics and its application to computer science in the form of formal methods. Currently, I am mostly using the theorem prover Isabelle/HOL and the programming language Haskell as a support in this endeavor.

In the past, I helped Dr. Achim Brucker and Dr. Burkhart Wolff with their project HOL-OCL. I was responsible for:

  • implementing the collection theories for lists, ordered sets, and multisets
  • lifting the generic Isabelle rewritter to do context-dependent rewritting with respect to the constructions employed in HOL-OCL

In my PhD studies, I am focusing on security protocol verification. I am especially interested in efficient verification techniques with strong soundness guarantees. Directions I am pursuing are:

  • automatic generation of machine-checked security proofs (cf. ESPL)
  • compositional verification techniques
  • design techniques resulting in security by construction (cf. talk about channel protocols)

I am also strongly interested in:

  • functional programming, as it makes programming as simple as mathematics.
  • (formal) logic, as it captures the essence of reasoning.