My research seeks to improve software reliability and security by developing new tools that help ensure correctness. My students and I tackle these problems on a variety of fronts, from fully formally verifying critical platforms like the web browser to developing novel algorithms that automatically check compiler optimizations. We draw on a diverse array of tools and techniques to address these challenges, including proof assistants, SMT solvers, translation validation, and type systems. While we spend many hours working out proofs on the whiteboard, we also like to get our hands dirty and build real, large systems. We get free food when we work late.
I'm extremely fortunate to work with some spectacular students:
|Spring 2014||CSE 341 : Programming Languages|
|Winter 2014||CSE 506 : Proof Assistants|
|Fall 2013||CSE 505 : Graduate Programming Languages|
The best way to reach me is in person. If my schedule doesn't say "busy", I'll be in CSE 546 or CSE 315. The next best way to reach me is over the phone and email works too.
My research interests include formal verification, compilers, and security. Even outside the lab, I try to code for fun most days. If I'm not hacking, I'm running long distances with friends, riding my bike around Seattle, painting badly, or playing board games. I can juggle and solve Rubik's cubes, but not at the same time. Also, my name has a wicked cool anagram.
I spent six sunny years at UC San Diego working on the PhD with my incredible advisor Sorin Lerner. Throughout grad school, Sorin set a stellar example of how remarkable research can be when you put students first, an example I strive to emulate. I also learned many invaluable lessons from the great Ranjit Jhala, especially when it comes to writing and presentation: Less is more!
I graduated from Purdue University back in Spring 2007 with degrees in Computer Science and Mathematics. As an undergraduate, I was fortunate to perform research with Suresh Jagannathan on the SML compiler MLton. For my Honors Project, advised by Antony Hosking, I designed and implemented a domain specific language to control a giant neon sculpture over the web. Over nearly three years, I ran the lab component of Purdue's introductory Java programming course.