Research themes
I use the interactive HOL4 theorem prover for nearly all my research. Interactive theorem provers (particularly LCF-style provers) are great at managing long and tedious proofs (that arise from software and hardware verification) and preventing users from accidentally proving false statements (which easily happens if verification is done by pen-and-paper). However, the interactive nature of these provers make them occasionally hard to use and cumbersome to apply. Much of my research has looked at how automation (often application-specific automation) can make interactive theorem provers easier to use, i.e. require less low-level interaction.
I've looked at automation that aids post-hoc program verification, and correct-by-construction synthesis from specifications in logic and, for practical purposes, combinations of the two. I've developed automation that eases verification/synthesis of machine code (ARM, x86, PowerPC) and functional programs (ML and Lisp), and have recently experimented with synthesis of hardware (for FPGAs).
To test whether the automation actually works, I usually attempt to apply it to medium to large scale case studies and, when possible, interface with other verification project that have been developed independently, e.g. L4.verified or Milawa.