ztatlock@cs.washington.edu
https://ztatlock.net
University of Washington, Seattle, WA
Paul G. Allen School of Computer Science & Engineering
Associate Professor, Autumn 2019 – Present
Assistant Professor, Autumn 2014 – Autumn 2019
Acting Assistant Professor, Autumn 2013 – Autumn 2014
Amazon Web Services, Seattle, WA
Automated Reasoning Group
Amazon Scholar, Autumn 2021 – Present
OctoML, Seattle, WA
Compiler Design and Implementation Group
Advisor, Autumn 2019 – Spring 2021
Microsoft Research India, Bengaluru, India
Systems Research Group
Graduate Research Intern, Summer 2010
University of California, San Diego, CA
PhD, Computer Science & Engineering, Autumn 2014
Thesis: Reducing the Costs of Proof Assistant Based Formal Verification
Advisor: Sorin Lerner
Purdue University, West Lafayette, IN
BS, Computer Science (Honors), Spring 2007
BS, Mathematics, Spring 2007
Advisor: Suresh Jagannathan
Brett Saiki, BS 2023
Andrew Cheung, BS 2023
Cynthia Richey, BS 2023
Andrew Liu, BS 2023
Mike He, BS 2022
Yihong Zhang, BS 2021
Adam Anderson, BS 2021
Taylor Blau, BS 2020
Josh Pollock, BS 2020
Altan Haan, BS 2020
Marisa Kirisame, BS 2019
Logan Weber, BS 2019
Jifan Zhang, BS 2019
David Thien, BS 2019
Paul Curry, BS 2018
Melissa Hovik, BS 2018
Justin Adsuara, BS 2018
Chen Qiu, BS 2018
Adam Geller, BS 2018
Steve Anton, BS 2017
Ryan Doenges, BS 2017
Miranda Edwards, BS 2017
Luke Nelson, BS 2017
Keith Simmons, BS 2017
Seth Pendergrass, BS 2016
Daryl Zuniga, BS 2015
Alex Sanchez-Stern, BS 2014
Better Together: Unifying Datalog and Equality Saturation
Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, Max Willsey
Programming Language Design and Implementation (PLDI) 2023
babble: Learning Better Abstractions with E-Graphs and Anti-Unification
David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, Nadia Polikarpova
Principles of Programming Languages (POPL) 2023
Small Proofs from Congruence Closure
Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, Pavel Panchekha
Formal Methods in Computer-Aided Design (FMCAD) 2022
Verified Compilation and Optimization of Floating-Point Programs in CakeML
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony Fox
European Conference on Object-Oriented Programming (ECOOP) 2022
Co-Optimization of Design and Fabrication Plans for Carpentry
Haisen Zhao, Max Willsey, Amy Zhu, Chandrakana Nandi, Zachary Tatlock, Justin Solomon, Adriana Schulz
ACM Transactions on Graphics (TOG) 2022
Relational e-matching
Yihong Zhang, Yisu Remy Wang, Max Willsey, Zachary Tatlock
Principles of Programming Languages (POPL) 2022
Rewrite Rule Inference Using Equality Saturation
Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2021
★ Distinguished Paper
A Roadmap Towards Parallel Printing for Desktop 3D Printers
Molly Aubrey Carton, Chandrakana Nandi, Adam Anderson, Haisen Zhao, Eva Darulova, Dan Grossman, Jeffrey I. Lipton, Adriana Schulz, Zachary Tatlock
Solid Freeform Fabrication Symposium (SFF) 2021
Combining Precision Tuning and Rewriting
Brett Saiki, Oliver Flatt, Chandrakana Nandi, Pavel Panchekha, Zachary Tatlock
IEEE International Symposium on Computer Arithmetic (ARITH) 2021
Pure Tensor Program Rewriting via Access Patterns
Gus Henry Smith, Andrew Liu, Steven Lyubomirsky, Scott Davidson, Joseph McMahan, Michael Taylor, Luis Ceze, Zachary Tatlock
Symposium on Machine Programming (MAPS) 2021
Dynamic Tensor Rematerialization
Marisa Kirisame, Steven Lyubomirsky, Altan Haan, Jennifer Brennan, Mike He, Jared Roesch, Tianqi Chen, Zachary Tatlock
International Conference on Learning Representations (ICLR) 2021
★ Spotlight Paper
Nimble: Efficiently Compiling Dynamic Neural Networks for Model Inference
Haichen Shen, Jared Roesch, Zhi Chen, Wei Chen, Yong Wu, Mu Li, Vin Sharma, Zachary Tatlock, Yida Wang
Conference on Machine Learning and Systems (MLSys) 2021
egg: Fast and Extensible Equality Saturation
Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, Pavel Panchekha
Principles of Programming Languages (POPL) 2021
★ Distinguished Paper
Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, Zachary Tatlock
Programming Language Design and Implementation (PLDI) 2020
Carpentry Compiler
Chenming Wu, Haisen Zhao, Chandrakana Nandi, Jeffrey I. Lipton, Zachary Tatlock, Adriana Schulz
SIGGRAPH Asia, ACM Transactions on Graphics (SIGA) 2019
Modular Verification of Web Page Layout
Pavel Panchekha, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2019
QED at Large: A Survey of Engineering of Formally Verified Software
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock
Foundations and Trends in Programming Languages (FTPL) 2019
Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler
Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock
Computer-Aided Verification (CAV) 2019
Teaching Rigorous Distributed Systems With Efficient Model Checking
Ellis Michael, Doug Woos, Thomas E. Anderson, Michael D. Ernst, Zachary Tatlock
European Conference on Computer Systems (EuroSys) 2019
Sinking Point: Dynamic Precision Tracking for Floating-Point
Bill Zorn, Dan Grossman, Zachary Tatlock
Conference for Next Generation Arithmetic (CoNGA) 2019
Functional Programming for Compiling and Decompiling Computer-aided Design
Chandrakana Nandi, James R. Wilcox, Pavel Panchekha, Taylor Blau, Dan Grossman, Zachary Tatlock
International Conference on Functional Programming (ICFP) 2018
Combining Tools for Optimization and Analysis of Floating-Point Computations
Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock
Formal Methods (FM) 2018
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB
Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen
Interactive Theorem Proving (ITP) 2018
Relay: a New IR for Machine Learning Frameworks
Jared Roesch, Steven Lyubomirsky, Logan Weber, Josh Pollock, Marisa Kirisame, Tianqi Chen, Zachary Tatlock
Machine Learning and Programming Languages (MAPL) 2018
Finding Root Causes of Floating Point Error
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
Programming Language Design and Implementation (PLDI) 2018
Verifying that Web Pages have Accessible Layout
Pavel Panchekha, Adam T. Geller, Michael D. Ernst, Zachary Tatlock, Shoaib Kamil
Programming Language Design and Implementation (PLDI) 2018
Programming and Proving with Distributed Protocols
Ilya Sergey, James R. Wilcox, Zachary Tatlock
Principles of Programming Languages (POPL) 2018
Œuf: Minimizing the Coq Extraction TCB
Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman
Certified Programs and Proofs (CPP) 2018
Automatic Formal Verification for EPICS
Jonathan Jacky, Stefani Banerian, Michael D. Ernst, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak
International Conference on Accelerator and Large Experimental Control Systems (ICALEPCS) 2017
SpaceSearch: A Library for Building and Verifying Solver-aided Tools
Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, Zachary Tatlock
International Conference on Functional Programming (ICFP) 2017
Programming Language Abstractions for Modularly Verified Distributed Systems
James R. Wilcox, Ilya Sergey, Zachary Tatlock
Summit oN Advances in Programming Languages (SNAPL) 2017
Programming Language Tools and Techniques for 3D Printing
Chandrakana Nandi, Anat Caspi, Dan Grossman, Zachary Tatlock
Summit oN Advances in Programming Languages (SNAPL) 2017
Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver
Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2016
Formal Semantics and Automated Verification for the Border Gateway Protocol
Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock
ACM SIGCOMM Workshop on Networking and Programming Languages (NetPL) 2016
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
Computer-Aided Verification (CAV) 2016
Verified Peephole Optimizations for CompCert
Eric Mullen, Daryl Zuniga, Zachary Tatlock, Dan Grossman
Programming Language Design and Implementation (PLDI) 2016
Planning for Change in a Formal Verification of the Raft Consensus Protocol
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas E. Anderson
Certified Programs and Proofs (CPP) 2016
Verdi: A Framework for Implementing and Formally Verifying Distributed Systems
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, Thomas E. Anderson
Programming Language Design and Implementation (PLDI) 2015
Automatically Improving Accuracy for Floating Point Expressions
Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, Zachary Tatlock
Programming Language Design and Implementation (PLDI) 2015
★ Distinguished Paper
RoboFlow: A Flow-based Visual Programming Language for Mobile Manipulation Tasks
Sonya Alexandrova, Zachary Tatlock, Maya Cakmak
International Conference on Robotics and Automation (ICRA) 2015
Toward a Dependability Case Language and Workflow for a Radiation Therapy System
Michael D. Ernst, Dan Grossman, Jonathan Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, Xi Wang
Summit oN Advances in Programming Languages (SNAPL) 2015
Visual Robot Programming for Generalizable Mobile Manipulation Tasks
Sonya Alexandrova, Zachary Tatlock, Maya Cakmak
Human Robot Interaction (HRI) 2015
Jitk: A Trustworthy In-Kernel Interpreter Infrastructure
Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock
Operating Systems Design and Implementation (OSDI) 2014
Automating Formal Proofs for Reactive Systems
Daniel Ricketts, Valentin Robert, Dongseok Jang, Zachary Tatlock, Sorin Lerner
Programming Language Design and Implementation (PLDI) 2014
SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks
Dongseok Jang, Zachary Tatlock, Sorin Lerner
Network and Distributed System Security (NDSS) 2014
Establishing Browser Security Guarantees through Formal Shim Verification
Dongseok Jang, Zachary Tatlock, Sorin Lerner
USENIX Security Symposium (SECURITY) 2012
Equality Saturation: A New Approach to Optimization
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
Logical Methods in Computer Science (LMCS) 2011
Bringing Extensibility to Verified Compilers
Zachary Tatlock, Sorin Lerner
Programming Language Design and Implementation (PLDI) 2010
Proving Optimizations Correct using Parameterized Program Equivalence
Sudipta Kundu, Zachary Tatlock, Sorin Lerner
Programming Language Design and Implementation (PLDI) 2009
Equality Saturation: A New Approach to Optimization
Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner
Principles of Programming Languages (POPL) 2009
Deep Typechecking and Refactoring
Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2008
Generate Compilers from Hardware Models!
Gus Henry Smith, Ben Kushigian, Vishal Canumalla, Andrew Cheung, René Just, Zachary Tatlock
Workshop on Programming Languages and Computer Architecture (PLARCH) 2023
Guarding Numerics Amidst Rising Heterogeneity
Ganesh Gopalakrishnan, Ignacio Laguna, Ang Li, Pavel Panchekha, Cindy Rubio-González, Zachary Tatlock
Software Correctness for HPC Applications (CORRECTNESS) 2021
From DSLs to Accelerator-Rich Platform Implementations: Addressing the Mapping Gap
Bo-Yuan Huang, Steven Lyubomirsky, Thierry Tambe, Yi Li, Mike He, Gus Henry Smith, Gu-Yeon Wei, Aarti Gupta, Sharad Malik, Zachary Tatlock
Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE) 2021
The Essence of Program Semantics Visualizers: A Three-Axis Model
Josh Pollock, Grace Oh, Eunice Jun, Philip J. Guo, Zachary Tatlock
Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU) 2020
Towards Numerical Assistants
Pavel Panchekha, Zachary Tatlock
Numerical Software Verification (NSV) 2020
Toward Multi-Precision, Multi-Format Numerics
David Thien, Bill Zorn, Pavel Panchekha, Zachary Tatlock
Software Correctness for HPC Applications (CORRECTNESS) 2019
Theia: Automatically Generating Correct Program State Visualizations
Josh Pollock, Jared Roesch, Doug Woos, Zachary Tatlock
ACM SIGPLAN International Symposium on SPLASH-E (SPLASH-E) 2019
Verification of Implementations of Distributed Systems Under Churn
Ryan Doenges, James R. Wilcox, Doug Woos, Zachary Tatlock, Karl Palmskog
Workshop on Coq for Programming Languages (CoqPL) 2017
Toward a Standard Benchmark Format and Suite for Floating-Point Analysis
Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alex Sanchez-Stern, Zachary Tatlock
Numerical Software Verification (NSV) 2016
Peek: A Formally Verified Peephole Optimization Framework for x86
Eric Mullen, Zachary Tatlock, Dan Grossman
Workshop on Coq for Programming Languages (CoqPL) 2015
Chapter 8: Parameterized Program Equivalence Checking
High-Level Verification: Methods and Tools for Verification of System-Level Designs
Sudipta Kundu, Sorin Lerner, and Rajesh K. Gupta; Springer 2011
UW CSE 505: Concepts of Programming Languages
Graduate course
using proof assistants to explore
transition systems,
inductive invariants,
type systems,
Hoare logic,
metatheory
UW CSE 341: Programming Languages
Undergraduate course exploring
informal operational semantics,
functional programming vs. OOP,
static vs. dynamic typing
UW CSE 331: Software Design and Implementation
Undergraduate course exploring
specification,
invariants,
testing,
debugging,
modular design
Special Topics Graduate Courses
★ I was honored to be nominated for the UW Distinguished Teaching Award in 2015.
UCSD CSE 231: Advanced Compiler Design
Graduate course exploring
program analyses and
compiler optimizations
UCSD CSE 130: Programming Languages
Undergraduate course exploring
functional programming,
static vs. dynamic typing, and
logic programming
Purdue CS 180: Introduction to Java Programming
Undergraduate course introducing students to Java programming:
variables,
conditionals,
loops,
recursion,
testing,
modular design, and
basic systems programming
Distinguished Paper Award for “Rewrite Rule Inference Using Equality Saturation”
ACM SIGPLAN Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2021
Spotlight Papaer Award for “Dynamic Tensor Rematerialization”
International Conference on Learning Representations (ICLR) 2021
Distinguished Paper Award for “egg: Fast and Extensible Equality Saturation”
ACM SIGPLAN Principles of Programming Languages (POPL) 2021
Faculty Appreciation for Career Education & Training (FACET) Award
University of Washington, 2020
NSF CAREER Award: Verifying Distributed System Implementations
National Science Foundation, 2017
Distinguished Paper Award for “Automatically Improving Accuracy for Floating Point Expressions”
ACM SIGPLAN Programming Language Design and Implementation (PLDI) 2015
Distinguished Teaching Award Nomination
University of Washington, 2015
The egg Equality Saturation Toolkit
UIUC, Compilers Seminar, May 2023
The egg Equality Saturation Toolkit
UC San Diego, Databases Seminar, March 2023
The egg Equality Saturation Toolkit
ETH Workshop on Dependable and Secure Software Systems, October 2022
Programming Languages for the Next Manufacturing Revolution
Department of Energy, July 2022
Towards Optimizing Multi-precision, Multi-format Numerical Codes
Intel ARITH, October 2020
Synthesizing Backward through the Geometry Pipeline
University of Wisconsin, PL Seminar, August 2020
Towards Numerical Assistants
Numerical Software Verification @ CAV, July 2020
TVM Relay: A Functional IR for Analysis and Optimization
TVM Conference, May 2019
Synthesis of Floating Point Programs and Beyond
Synthetic Minds, September 2019
Verifying Implementations of Distributed Systems
Galois Inc., September 2018
Formally Verifying Implementations of Distributed Systems
Princeton University, DeepSpec Summer School, July 2018
Formally Verifying Implementations of Distributed Systems
Oxford University, Coq Workshop at FLOC, July 2018
Navigating Your Career Path
Programming Languages Mentoring Workshop (PLMW), June 2018
The FPBench Suite and Specification
Dagstuhl on Analysis and Synthesis of Floating-point Programs, August 2017
Automatically Improving the Accuracy of Floating Point Expressions
Max Planck Institute (MPI-SWS Saarbrüken), August 2017
Verifying Control Plane Policies in BGP
Mathematical Foundations of Programming Semantics (MFPS), June 2017
Automated Formal Verification for Border Gateway Protocol Configurations
Purdue University, April 2017
Automatically Improving the Accuracy of Floating Point Expressions
University of Utah, February 2017
Dijkstra and De Millo: Challenges in Applying and Teaching Verification
Microsoft Research Faculty Summit, July 2016
Verifying Safety Cases for Radiotherapy Control
Verified Software: Theories, Tools, and Experiments (VSTTE), June 2016
I have also helped write, produce, and direct UW’s annual faculty skit since 2015 with Hank Levy and Adriana Schulz.
ComPort: Rigorous Testing Methods to Safeguard Software Porting
Co-PI; DOE; $405,000; 2021 – 2024
V-SPELLS: POLYMORPH: Promotion to Optimal Languages Yielding Modular Operator-driven Replacements and Programmatic Hooks
Co-PI; DARPA; $746,365; 2021 – 2024
FMitF: Retargetable, Verifiable, Optimizable Computer-Aided Manufacturing
Co-PI; NSF CCF-2017927; $749,913; 2020 – 2023
RTML: Automatic Synthesis of HW/SW Systems for General Neural-Networks
Co-PI; DARPA; $2,803,490; 2019 – 2022
Knit Pattern Understanding for Garment Modeling, Modification, and Fabrication
Co-PI; NSF CHS-1907337; $500,000; 2019 – 2021
FMitF: Formal Verification of Accessibility
Co-PI; NSF CCF-1836813; $738,125; 2019 – 2022
Programming Languages Foundations for 3D Printing
PI; NSF SHF-1813166; $500,000; 2018 – 2021
Applications Driving Architectures (ADA) SRC JUMP Center
Co-PI; Joint SRC & DARPA; $580,000; 2018 – 2022
CAREER: Verifying Distributed Systems Implementations
PI; NSF CCF-1749570; $550,000; 2018 – 2023
BRASS: A Picture is Worth a Billion Bits: Adaptive Visualization of Big Data
Co-PI; DARPA; $7,500,000; 2015 – 2019