I am interested in finding bugs in programs, large and small, and sometimes proving them correct. I like formal verification techniques and semantics of programming languages, especially if they are compositional.
Here be wyverns! Verifying LLVM IR with llStar. . [Draft | slides]