zachary tatlock
Zachary Tatlock
ztatlock@cs.washington.edu
Assistant Professor
Computer Science and Engineering
University of Washington

Research

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.

Projects

Peek investigates formally verifying assembly-level optimizations in CompCert. [PLDI 16, CoqPL 15]

Verdi provides a framework for formally verifying implementations of distributed systems. [CPP 16, PLDI 15]

Herbie automatically improves the numerically accuracy of floating-point programs. [PLDI 15]

Bagpipe verifies the BGP router configurations that ISPs use to select and propagate routing information across the Internet. [NetPL 16]

Neutrons develops techniques to ensure the correctness of a radiotherapy device in the UW Clinical Neutron Therapy System. [CAV 16, SNAPL 15]

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.

Students

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:

Teaching

CSE 599W : Systems Verification
Sp 16
CSE 331 : Software Design and Implementation
Wi 16
CSE 505 : Graduate Programming Languages
Fa 15
CSE 341 : Programming Languages
Sp 15
CSE 505 : Graduate Programming Languages
Wi 15
CSE 341 : Programming Languages
Sp 14
CSE 506 : Proof Assistants
Wi 14
CSE 505 : Graduate Programming Languages
Fa 13
I was honored to be nominated for the UW Distinguished Teaching Award in 2015.

Contact

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.

Background

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.

Misc.

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: