My primary research focuses on applications of formal logic to computer science. This includes: automated theorem proving and SAT/SMT solving; formal systems for program verification (i.e., Hoare logic, dynamic logic, separation logic); and of course, just logic for logic's sake.

I also am interested in programming language design and implementation, and whenever possible, I prefer to program in functional languages. Some of my favorites are OCaml, Haskell and Lisp.