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.
- 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.