zachary tatlock
Zachary Tatlock
Assistant Professor
Computer Science and Engineering
University of Washington


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.


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: 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):

After graduating, students go on to awesome new opportunities:

I am also very lucky to work on projects with these sharp folks:


CSE 505 : Graduate Programming Languages
Fa 17
CSE 599Z : Accurate Computing
Sp 17
CSE 331 : Software Design and Implementation
Wi 17
CSE 505 : Graduate Programming Languages
Fa 16
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.


The best way to reach me is by email. If you send a message and I do not reply within 24 hours, please resend and CC

Other Stuff...