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: RoboFlow, 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:
If you send an email and I do not reply within 24 hours, please resend your message and cc firstname.lastname@example.org.