Computer programming is a huge success; it plays a major role in all modern problem solving. However, for some problems we still have trouble writing programs that reliably do the right thing. My research improves software reliability by developing tools that help programmers ensure their code is safe and accurate.
My students and I focus on important programs, including the software infrastructure that many other programs rely on (compilers, distributed systems, networks, web browsers); control programs in safety-critical applications (radiotherapy devices, robotics); and approximations used in engineering and manufacturing (floating point, 3D printing). We spend many hours working out proofs on the whiteboard, but we always build working systems.
All our papers (scholar, dblp) and projects are collaborations with incredible colleagues, often in the PLSE and Systems and Networking groups at UW. We release our code so others can review and build on our work. We also get free food when we work late.
Incarnate applies ideas from compiler verifiation and numerical methods to improving the accuracy of desktop 3D printers.
Darknet is an open source neural network framework written in C and CUDA. It is fast, easy to install, and supports CPU and GPU computation.
FPBench is a new standard for floating-point accuracy benchmarks.
Checking out some past projects can also help provide a sense for the sort of work we do: Jitk, Reflex, SafeDispatch, Quark, Peggy, PEC/XCert, Quail.
I'm extremely fortunate to advise some spectacular graduate students:
As well as some stellar undergraduate students (co-advised with my graduate students):
And also very lucky to work on active projects with these sharp folks:
The best way to reach me is in person. If my schedule doesn't say "busy", I'll be in CSE 546 or CSE 407.
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.
My friend Garbo and I run Seattle's premier pizza haiku blog: Seattle Pizza Odyssey.
Emina and I made a video about the Neutrons project!
Once, while interning at MSR India, I got to drive an auto rickshaw.
Some folks in the department juggle stuff.
We also have a great running group that trots all over the city.
We made a cool video showing how Roboflow works.
Seattle is epic; some of our adventures show up on social media stuff: