- formal development methods
- specification, modeling and design of reliable software
- theories of programming, refinement calculi, concurrency
- foundations of software testing.
His current research is mainly concerned with the automated generation of test-cases from formal requirements specifications as well as with the associated testing theories. This includes the investigation of existing testing, specification and refinement techniques. The aim is to develop testing theories that are able to unify the existing results on specification-based testing and advance the field.His current emphasis is on fault-based testing. Fault-based testing is a technique where testers anticipate errors in a system under test in order to asses or generate test cases. The idea is to have enough test cases capable of detecting these anticipated errors. He applies this method on the specification level. His latest testing theory is based on Hoare and He's Unifying Theory of Programming (UTP) and has been instantiated to test case generator’s for OCL, Spec#, LOTOS and most recently Action Systems.