Zachary Tatlock

Zachary Tatlock

ztatlock@cs.washington.edu
Assistant Professor
Allen School of Computer Science and Engineering
University of Washington

Research

Computer programming is a huge success; it plays a major role in most 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); control programs in safety-critical applications (radiotherapy devices); 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 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.

Students

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:

Co-advised with (1) Dan Grossman, (2) Michael D. Ernst, (3) Tom Anderson, (4) Xi Wang

Projects

OEUF_LOGO Oeuf explores verified compilation from a subset of Gallina (Coq’s functional programming language) to the CompCert Cminor intermediate representation to enable trustworthy binary executable code generation for Coq. [CPP 18]
DISCO_LOGO The Distributed Components project aims to provide modular verified components for distributed systems. [POPL 18, SNAPL 17]
INCARNATE_LOGO Incarnate applies ideas from compiler verifiation and numerical methods to improve the reliability of desktop 3D printers. [SNAPL 17]
CASSIUS_LOGO Cassius develops tools to automatically reason about web page layout and help developers ensure their pages are accessible to everyone. [PLDI 18]
HERBGRIND_LOGO Herbgrind builds on Valgrind to provide binary instrumentation for dynamically identifying the root cause of floating-point inaccuracy in large, low-level numerical programs. [PLDI 18]
NEUTRONS_LOGO Neutrons develops techniques to ensure the correctness of radiotherapy devices in the UW Clinical Neutron Therapy System. [ICALEPCS 17, CAV 16, SNAPL 15]
VERDI_LOGO Verdi provides a framework for formally verifying implementations of distributed systems. [CPP 16, PLDI 15]
HERBIE_LOGO Herbie automatically improves the numerically accuracy of floating-point programs. [PLDI 15]
FPBENCH_LOGO FPBench provides a set of tools and community standard for floating-point accuracy benchmarks. [NSV 16]

Checking out past projects can also help provide a sense for the sort of work we do:

Teaching

Wi 18 CSE 341: Programming Languages
Fa 17 CSE 505: Graduate Programming Languages
Sp 17 CSE 599Z: Accurate Computing
Wi 17 CSE 331: Software Design and Implementation
Fa 16 CSE 505: Graduate Programming Languages
Sp 16 CSE 599W: Systems Verification
Wi 16 CSE 331: Software Design and Implementation
Fa 15 CSE 505: Graduate Programming Languages
Sp 15 CSE 341: Programming Languages
Wi 15 CSE 505: Graduate Programming Languages
Sp 14 CSE 341: Programming Languages
Wi 14 CSE 506: Proof Assistants
Fa 13 CSE 505: Graduate Programming Languages

I was honored to be nominated for the UW Distinguished Teaching Award in 2015.

Publications

PLDI 18 Verifying that Web Pages have Accessible Layout
Pavel Panchekha, Adam Geller, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil
project
 
PLDI 18 Finding Root Causes of Floating Point Error
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
project
 
CPP 18 Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman
project  
 
POPL 18 Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, Zachary Tatlock
project  
 
ICFP 17 Spacesearch: A Library for Building and Verifying Solver-aided Tools
Konstantin Weitz, Steven Lyubomirsky, Stefan Heule,
Emina Torlak, Michael D. Ernst, Zachary Tatlock
project  
 
ICALEPCS 17 Automatic Formal Verification for EPICS
Jonathan Jacky, Stefani Banerian, Michael D. Ernst, Calvin Loncaric,
Stuart Pernsteiner, Zachary Tatlock, Emina Torlak
project   talk   pdf slides   bib   publisher
 
SNAPL 17 Programming Language Tools and Techniques for 3D Printing
Chandrakana Nandi, Anat Caspi, Dan Grossman, Zachary Tatlock
project  
 
SNAPL 17 Programming Language Abstractions for Modularly Verified Distributed Systems
James R. Wilcox, Ilya Sergey, Zachary Tatlock
project  
 
COQPL 17 Verification of Implementations of Distributed Systems Under Churn
Ryan Doenges, James R. Wilcox, Doug Woos, Zachary Tatlock, Karl Palmskog
project  
 
OOPSLA 16 Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver
Konstantin Weitz, Doug Woos, Emina Torlak,
Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock
project  
 
NSV 16 Toward a Standard Benchmark Format and Suite for Floating-point Analysis
Nasrine Damouche, Matthieu Martel, Pavel Panchekha,
Chen Qiu, Alexander Sanchez-Stern, Zachary Tatlock
project   talk   pdf slides
 
NETPL 16 Formal Semantics and Automated Verification for the Border Gateway Protocol
Konstantin Weitz, Doug Woos, Emina Torlak,
Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock
project  
 
CAV 16 Investigating Safety of a Radiotherapy Machine using System Models with Pluggable Checkers
Stuart Pernsteiner, Calvin Loncaric, Emina Torlak,
Zachary Tatlock, Xi Wang, Michael D. Ernst, Jonathan Jacky
project  
 
PLDI 16 Verified Peephole Optimizations for CompCert
Eric Mullen, Daryl Zuniga, Zachary Tatlock, Dan Grossman
project   talk  
 
CPP 16 Planning for Change in a Formal Verification of the Raft Consensus Protocol
James R. Wilcox, Doug Woos, Steve Anton,
Zachary Tatlock, Michael D. Ernst, Tom Anderson
project   pdf slides  
 
SNAPL 15 Toward a Dependability Case Language and Workflow for a Radiation Therapy System
Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric,
Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, Xi Wang
project   pdf slides  
 
PLDI 15 Automatically Improving Accuracy for Floating Point Expressions
Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, Zachary Tatlock
project   video abstract   talk   poster   pdf slides
Distinguished Paper Award
 
PLDI 15 Verdi: A Framework for Implementing and Formally Verifying Distributed Systems
James R. Wilcox, Doug Woos, Pavel Panchekha,
Zachary Tatlock, Xi Wang, Michael D. Ernst, Tom Anderson
project   pdf slides  
 
HRI 15 Visual Robot Programming for Generalizable Mobile Manipulation Tasks
Sonya Alexandrova, Zachary Tatlock, Maya Cakmak
project
 
ICRA 15 RoboFlow: A Flow-based Visual Programming Language for Mobile Manipulation Tasks
Sonya Alexandrova, Zachary Tatlock, Maya Cakmak
project
 
COQPL 15 Peek: A Formally Verified Peephole Optimization Framework for x86
Eric Mullen, Zachary Tatlock, Dan Grossman
project
 
OSDI 14 Jitk: A Trustworthy In-Kernel Interpreter Infrastructure
Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock
project   talk   slides
 
PLDI 14 Automating Formal Proofs for Reactive Systems
Daniel Ricketts, Valentin Robert, Dongseok Jang, Zachary Tatlock, Sorin Lerner
project   talk   pdf slides   slides
 
NDSS 14 SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks
Dongseok Jang, Zachary Tatlock, Sorin Lerner
pdf slides   slides
 
SECURITY 12 Establishing Browser Security Guarantees Through Formal Shim Verification
Dongseok Jang, Zachary Tatlock, Sorin Lerner
project   poster   talk   slides
 
LMCS 11 Equality Saturation: A New Approach to Optimization
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
project
 
PLDI 10 Bringing Extensibility to Verified Compilers
Zachary Tatlock, Sorin Lerner
project   slides
 
PLDI 09 Proving Optimizations Correct Using Parameterized Program Equivalence
Sudipta Kundu, Zachary Tatlock, Sorin Lerner
project   talk   slides
 
POPL 09 Equality Saturation: A New Approach to Optimization
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
project   talk   slides
 
OOPSLA 08 Deep Typechecking and Refactoring
Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
project   poster   slides

Similar listings are available at: DBLP, Google Scholar, Semantic Scholar, Research Gate

Service

Reviewing:

Collaborators

I have been very fortunate to work on projects with some amazing folks over the years:

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 with friends or making something. 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 our Honors Project, advised by Antony Hosking, Bill Harris and 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

Some things worth reading:

We have a great running group, Race Condition Running, that trots all over the city and gets brunch each week.

race condition running

I help out with a bunch of stuff around the Allen School, including TGIF. Sometimes super famous guests swing by :) Check out all our TGIF photos!

david walker and zach tatlock uw cse tgif

In summer 2017, Pavel and I met with a bunch of great folks at a Dagstuhl on Floating Point.

2017 floating point dagstuhl

Emina and I made video about Neutrons.

We made a cool video showing how Roboflow works.

My friend Garbo and I run Seattle’s premier pizza haiku blog: Seattle Pizza Odyssey.

Some folks in the department juggle stuff.

ztatlock juggling

We teach many important life skills here in the Allen School.

UCSD’s 2014 Holiday Party featured an inspirational ad, and Ed noticed.

Once while interning at MSR India, I got to drive an auto rickshaw.

ztatlock rickshaw

My academic genealogy:

The best bound I know on my Erdős number, is 4 via James Wilcox:

ztatlock erdos number