Research of Personal Interest

I'm generally interested in the use of formal methods in informatics (computer science) in particular for building safe and secure systems. This includes methods and tools for designing, specifying, valdidating and verifying hardware and software 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.
• 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.