I'm a second year PhD student at the University of Washington, advised by Dan Grossman and Luis Ceze. I work in both the PLSE and Sampa groups. I'm interested in applying formal methods to understand how processors work at a very low level.
My current research project is an effort to bring high-level formal techniques, such as proofs of code correctness, closer to real, physical hardware. I'm working on a system that can model, learn, and validate low-level properties of the TI MSP430 ISA, such as the timing behavior of the instructions. The goal is to produce a tool that is automated, flexible enough to be extended to new ISAs and properties, and that can provide strong guarantees about code, such as resistance to side-channel attacks on specific hardware implementations.
I greatly enjoy training deep, recurrent neural networks as character-level language models. There's a fantastic blog post about it here.
One particularly interesting application is generating Magic: the Gathering cards. There's a huge forum thread about it (I didn't start the thread, though I've contributed under the handle hardcast_sixdrop). I've also written a tutorial.