Formally verifying that a system conforms to a specification is a challenging problem in computer science. It is so challenging, that there are instances of the problem that are classified as undecidable. Yet, over the past two decades this field of research has seen great advancements.

Here are some of the topics I am interested in:

1. Core model checking algorithms for both hardware and software systems.
2. Applications of formal verification techniques for security verification.
3. SAT and SMT solving.
4. Abstraction techniques.