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.

Other Stuff...