I am a researcher (post-doc) at the chair for logic and verification of Prof. Tobias Nipkow. My main research interest is the production of verified software by a top-down refinement process. For this, I’m using the theorem prover Isabelle/HOL, for which I have developed the Isabelle Refinement Framework and the Isabelle Collection Framework. Other research interests include the automatic analysis of models for concurrent programs, and the mechanical verification of the analysis algorithms. To this end, I have explored dynamic pushdown networks, a model for concurrent programs with thread creation and locks as synchronization primitive. Moreover, we have developed the fully verified CAVA LTL model checker. Recently, I have also worked on modeling web-services in Isabelle/HOL, and formally verifying their information flow security properties. As a demonstrator, we have developed the conference management system CoCon, that has formally verified information flow properties