Research of Personal Interest

I am generally interested in the use of formal methods in computer science in particular for building safe and secure systems. This includes the development of methods and tools for designing, specifying, validating and verifying hardware and software systems.

My research interests comprise the three areas System Engineering, Safety and Security, and Formal Methods. Here, my interests range from basic research to applied research and, consequently, I am particularly keen in applying basic research results in industrial environments.

Ongoing work includes, among others, research in the following areas:

• Specification-based testing for functional and non-functional (e.g., security testing) testing
• Formal semantics and theorem provers for object-oriented systems
• Static code analysis for ensuring the security of software applications
• Modeling, analyzing, and executing security or safety critical business processes
• Access control models and techniques for service-oriented systems

Recent Activities:

• Co-maintaining Isabelle/HOL-Z, an integrated proof environment for the Z formalism; see the HOL-Z hompage for more information.
• Developing Isabelle/HOL-OCL, an proof environment for UML/OCL specifications. More information can be found on the HOL-OCL site.
• Developing HOL-TestGen, a test case generator. More information can be found on the HOL-TestGen site.
• Developing Isabelle/OFMC, a protocol verification tool based on Isabelle/HOL and OFMC. More information can be found on the Isabelle/OFMC site.
• As a service to the theorem proving community, I'm offering IsaMorph which is a ready-to-run Linux CD featuring the interactive theorem prover Isabelle. More information can be found on the IsaMorph site.