ztatlock
A zebra with sunglasses and laser eyes spelling Z.

Advising and Mentoring

Current Postdoctoral Researchers

Max Willsey

Max Willsey

🚀

Joined 2021

🔎

Fast and Flexible Equality Saturation

Current PhD Students

Yihong Zhang

Yihong Zhang

🚀

Joined 2022

âž•

Co-advised with Dan Suciu

🔎

Equality Saturation in Datalog

Oliver Flatt

🚀

Joined 2022

🔎

Automated Numerical Accuracy Improvement

🔎

Efficient Proofs for Congruence Closure

Kevin Mu

🚀

Joined 2022

âž•

Co-advised with Adriana Schulz

🔎

Fast and Accurate Numerical Kernels

Anjali Pal

Anjali Pal

🚀

Joined 2022

🔎

Scaling Rewrite Rule Synthesis

Amy Zhu

Amy Zhu

🚀

Joined 2020

âž•

Co-advised with Adriana Schulz

🔎

PL and Design Optimization for Knitting

Gus Henry Smith

Gus Henry Smith

🚀

Joined 2018

âž•

Co-advised with Luis Ceze

🔎

Hardware Software Co-design for ML Accelerators

Current Bachelors Students

Ryan Tjoa

🚀

Joined 2023

âž•

Co-advised with Yihong Zhang, Oliver Flatt

🔎

Automated Theorem Proving with Egglog

Kevin Yan

🚀

Joined 2023

âž•

Co-advised with Yhong Zhang

🔎

Fast and Flexible Equality Saturation

Thia Richey

🚀

Joined 2022

🔎

Scaling Rewrite Rule Synthesis

Cynthia Richey

🚀

Joined 2022

âž•

Co-advised with Anjali Pal

🔎

Scaling Rewrite Rule Synthesis

Andrew Cheung

🚀

Joined 2022

âž•

Co-advised with Gus Henry Smith

🔎

Hardware Software Co-design for ML Accelerators

Vishal Canumalla

Vishal Canumalla

🚀

Joined 2021

âž•

Co-advised with Gus Henry Smith

🔎

Hardware Software Co-design for ML Accelerators

Brett Saiki

Brett Saiki

🚀

Joined 2019

âž•

Co-advised with Pavel Panchekha, Bill Zorn

🔎

Optimizing Mixed-precision Numerical Accuracy

Graduated PhD Students

Steven Lyubomirsky

Steven Lyubomirsky

🎓

PhD 2022

🔎

ML Compiler Design (TVM Relay)

🔎

Dynamic Tensor Rematerialization

📜

Compiler and Runtime Techniques for Optimizing Deep Learning Applications

⮕

Senior Machine Learning Systems Engineer at OctoML

Chandrakana Nandi

Chandrakana Nandi

🎓

PhD 2021

âž•

Co-advised with Dan Grossman

🔎

PL for 3D Printing and CAD

🔎

Rewrite Rule Synthesis

📜

Programming Language Tools and Techniques for Computational Fabrication

⮕

Senior Researcher and Formal Verification Lead at Certora

Bill Zorn

Bill Zorn

🎓

PhD 2021

âž•

Co-advised with Dan Grossman

🔎

Number Systems Analysis and Optimization

📜

Rounding

⮕

Numerical Hardware Architect at Intel

James R. Wilcox

James R. Wilcox

🎓

PhD 2021

🔎

Formal Verification of Distributed Systems

🔎

Automatic Inductive Invariant Inference

📜

Compositional and Automated Verification of Distributed Systems

⮕

CTO at Certora (2019)

⮕

Assistant Teaching Professor at the University of Washington

Jared Roesch

Jared Roesch

🎓

PhD 2020

🔎

ML Compiler Design (TVM Relay)

📜

Principled Optimization Of Dynamic Neural Networks

⮕

Co-founder and CTO at OctoML

Pavel Panchekha

Pavel Panchekha

🎓

PhD 2019

âž•

Co-advised with Michael D. Ernst

🔎

Web Page Layout Verification

🔎

Automated Numerical Accuracy Improvement

📜

Automated Reasoning for Web Page Layout

⮕

Assistant Professor at the University of Utah

Doug Woos

Doug Woos

🎓

PhD 2019

âž•

🔎

Formal Verification and Interactive Visualization of Distributed Systems

📜

A Step-through Debugger for Distributed Systems

⮕

Lecturer at Brown University

Eric Mullen

Eric Mullen

🎓

PhD 2018

âž•

Co-advised with Dan Grossman

🔎

Formal Verification of Peephole Optimizations in CompCert

📜

Pushing the Limits of Compiler Verification

⮕

Google

Stuart Pernsteiner

Stuart Pernsteiner

🎓

PhD 2018

âž•

Co-advised with Michael D. Ernst

🔎

Formal Verificaton and Analysis of Radiotherapy Control Systems

📜

Practical Verification of Safety-Critical Systems

⮕

Galois

Konstantin Weitz

Konstantin Weitz

🎓

PhD 2017

âž•

Co-advised with Michael D. Ernst

🔎

Formal Verification of Border Gateway Protocol (BGP) Configurations

📜

Formal Semantics and Scalable Verification for the Border Gateway Protocol using Proof Assistants and SMT Solvers

⮕

Google

⮕

Co-founder at Nexus

Graduated Masters Students

Yihong Zhang

Yihong Zhang

🎓

MS 2022

🔎

Congruence + Relational Databases

⮕

PhD Student at the University of Washington

Marisa Kirisame

Marisa Kirisame

🎓

MS 2020

🔎

Dynamic Tensor Rematerialization

⮕

PhD Student at the University of Utah

Logan Weber

Logan Weber

🎓

MS 2020

🔎

Embedded ML Runtime Systems

⮕

PhD Student at MIT

Alex Sanchez-Stern

Alex Sanchez-Stern

🎓

MS 2015

🔎

Dynamic Numerical Error Analysis

⮕

PhD Student at UC San Diego

Graduated Bachelors Students

David Cao

🎓

BS 2022

🔎

Library Learning with E-graphs and Antiunification (Summer RA)

Andrew Liu

Andrew Liu

🎓

BS 2022

âž•

Co-advised with Gus Henry Smith

🔎

Custom Numeric Datatypes for ML Training

Mike He

Mike He

🎓

BS 2022

âž•

Co-advised with Steven Lyubomirsky

🔎

Dynamic Tensor Rematerialization

⮕

PhD Student at Princeton University

Adam Anderson

Adam Anderson

🎓

BS 2021

âž•

Co-advised with Chandrakana Nandi

🔎

Rewrite Rule Synthesis

Yihong Zhang

Yihong Zhang

🎓

BS 2021

🔎

Relational E-matching

📜

Relational E-matching

⮕

MS Student at the University of Washington

Taylor Blau

Taylor Blau

🎓

BS 2020

âž•

Co-advised with Talia Ringer

🔎

PL for 3D Printing

📜

Verifying Strong Eventual Consistency in δ-CRDTs

⮕

GitHub

Josh Pollock

Josh Pollock

🎓

BS 2020

âž•

Co-advised with Jared Roesch, Doug Woos

🔎

Program State Visualization

🔎

ML Compiler Design (TVM Relay)

📜

Sidewinder: Designing Correct Program State Visualizations

⮕

PhD Student at MIT

Altan Haan

Altan Haan

🎓

BS 2020

âž•

Co-advised with Jared Roesch, Steven Lyubomirsky

🔎

Dynamic Tensor Rematerialization

🔎

ML Compiler Design (TVM Relay)

📜

Simulating Dynamic Tensor Rematerialization

⮕

OctoML

⮕

PhD Student at UC Berkeley

Marisa Kirisame

Marisa Kirisame

🎓

BS 2019

âž•

Co-advised with Jared Roesch

🔎

ML Compiler Design (TVM Relay)

⮕

MS Student at the University of Washington

Logan Weber

Logan Weber

🎓

BS 2019

âž•

Co-advised with Jared Roesch

🔎

ML Compiler Design (TVM Relay)

⮕

MS Student at the University of Washington

Jifan Zhang

Jifan Zhang

🎓

BS 2019

🔎

ML Compiler Design (TVM Relay)

⮕

MS Student at the University of Washington (w/ Kevin Jamieson)

⮕

PhD Student at the University of Wisconsinn

David Thien

🎓

BS 2019

âž•

Co-advised with Pavel Panchekha

🔎

Automated Numerical Accuracy Improvement

⮕

PhD Student at UCSD

Paul Curry

🎓

BS 2018

🔎

PL for 3D Printing

⮕

Xnor.ai

⮕

Apple

Melissa Hovik

Melissa Hovik

🎓

BS 2018

🔎

PL for 3D Printing

⮕

MS Student and Instructor at the University of Washington

⮕

Instructor at CalTech

Justin Adsuara

🎓

BS 2018

âž•

Co-advised with Doug Woos

🔎

Verification of Distributed Systems Under Churn

🔎

Formally Verified Serialization

⮕

Hilton Hotels

Chen Qiu

🎓

BS 2018

âž•

Co-advised with Pavel Panchekha

🔎

Automated Numerical Accuracy Improvement

⮕

MS Student at the University of Washington

⮕

Facebook

Adam T. Geller

🎓

BS 2018

âž•

Co-advised with Pavel Panchekha

🔎

CSS Formalization in SMT

🔎

Web Page Layout Verification

⮕

PhD Student at the University of British Columbia

Steve Anton

🎓

BS 2017

âž•

Co-advised with James R. Wilcox, Doug Woos

🔎

Formally Verified Distributed Systems

⮕

Google

Ryan Doenges

🎓

BS 2017

âž•

Co-advised with James R. Wilcox, Doug Woos

🔎

Formal Verification of Distributed Systems Under Churn

⮕

PhD Student at Cornell University

Miranda Edwards

🎓

BS 2017

âž•

Co-advised with James R. Wilcox

🔎

Formally Verified Distributed Systems

⮕

Cisco Meraki

Luke Nelson

🎓

BS 2017

âž•

Co-advised with Xi Wang

🔎

Formally verified

🔎

self-hosted eBPF JIT Compilation

⮕

PhD Student at the University of Washington

Keith Simmons

🎓

BS 2017

âž•

Co-advised with James R. Wilcox, Doug Woos

🔎

Formally Verified Distributed Systems

⮕

Microsoft

Seth Pendergrass

Seth Pendergrass

🎓

BS 2016

🔎

PL for 3D Printing

⮕

Microsoft

⮕

Oculus VR

Daryl Zuniga

Daryl Zuniga

🎓

BS 2015

âž•

Co-advised with Eric Mullen, Dan Grossman

🔎

Formal Verification of Peephole Optimizations in CompCert

⮕

Microsoft

Alex Sanchez-Stern

Alex Sanchez-Stern

🎓

BS 2014

âž•

Co-advised with Pavel Panchekha

🔎

Automated Numerical Accuracy Improvement

⮕

MS Student at the University of Washington

Graduated High School Students

Grace Oh

Grace Oh

🎓

HS 2021

âž•

Co-advised with Josh Pollock, Eunice Jun

🔎

Program State Visualization

🔎

CS Education

⮕

BA Student at Princeton University

Adam Anderson

Adam Anderson

🎓

HS 2018

âž•

Co-advised with Chandrakana Nandi

🔎

PL for 3D Printing

⮕

BS Student at the University of Washington

Juliet Oh

🎓

HS 2016

🔎

PL for 3D Printing

⮕

BA Student at Princeton University