I am interested in formal methods for the correct construction of hardware and software sys­tems, with a focus on automated methods for checking compliance of an implementation with a specification. Techniques include model checking and automated testing. I am particularly interested in applying these methods to practical hard- and software im­ple­mentations given in languages like C/C++/Java, or HDLs such as Verilog and SystemC.