Amy Zhu
Co-advised with Adriana Schulz
Joined Summer 2020

• Rewrite Synthesis
• PL for Knitting

Gus Smith
Co-advised with Luis Ceze
Joined Autumn 2018

• Custom Numeric Datatypes for ML Training
• Hardware Software Co-design for ML Accelerators

Steven Lyubomirsky
Joined Autumn 2016

• ML Compiler Design (TVM Relay)
• Dynamic Tensor Rematerialization

Chandrakana Nandi
Co-advised with Dan Grossman
Joined Autumn 2015

• Rewrite Synthesis
• PL for 3D Printing and Carpentry

Jared Roesch
Joined Autumn 2015

• ML Compiler Design (TVM Relay)
• OctoML

Bill Zorn
Co-advised with Dan Grossman
Joined Autumn 2014

• Floating-point Accuracy
• Number Systems Analysis Tools

Andrew Liu
Co-advised with Gus Smith
Joined Summer 2020

• Custom Numeric Datatypes for ML Training
• Hardware Software Co-design for ML Accelerators

Brett Saiki
Co-advised with Bill Zorn and Pavel Panchekha
Joined Winter 2019

• Floating-point Accuracy
• Mixed-precision Optimization

Mike He
Co-advised with Steven Lyubomirsky
Joined Winter 2019

• ML Compiler Design (TVM Relay)
• Dynamic Tensor Rematerialization

Adam Anderson
Co-advised with Chandrakana Nandi
Joined Summer 2017 (HS)

• Rewrite Synthesis
• PL for 3D Printing

Grace Oh
Co-advised with Josh Pollock and Eunice Jun
Joined Summer 2020

• Program State Visualization
• CS Education

Pavel Panchekha
Co-advised with Michael D. Ernst
PhD 2019 → Assistant Professor at Utah

• Web Page Layout Verification
• Automatic Floating-point Accuracy Improvement

James R. Wilcox
ABD 2019 → CTO at Certora

• Formal Verification of Distributed Systems
• Automatic Inductive Invariant Inference

Doug Woos
Co-advised with Michael D. Ernst and Thomas E. Anderson
PhD 2019 → Lecturer at Brown

• Formal Verification of Distributed Systems
• Distributed Systems Visualization

Stuart Pernsteiner
Co-advised with Michael D. Ernst
PhD 2018 → Galois Inc. 

• Radiotherapy Control System Analysis and Reliability
• Formal Verification of Coq-to-x86 Compilation

Eric Mullen
Co-advised with Dan Grossman
PhD 2018 → Google

• Formal Verification of Peephole Optimizations for CompCert
• Formal Verification of Coq-to-x86 Compilation

Konstantin Weitz
Co-advised with Michael D. Ernst
PhD 2017 → Google

• Formal Verification of Border Gateway Protocol Router Configurations
• Formal Verification of Solver-aided Tools

Marisa Kirisame
BS 2019, MS 2020 → PhD Student at Utah

• Dynamic Tensor Rematerialization
• ML Compiler Design (TVM Relay)

Logan Weber
BS 2019, MS 2020 → PhD Student at MIT

• Embedded ML Runtime Systems
• ML Compiler Design (TVM Relay)

Alex Sanchez-Stern
BS 2014, MS 2015 → PhD Student at UCSD

• Automatic Floating-point Accuracy Improvement
• Dynamic Floating-point Error Analysis

Altan Haan
BS 2020 → OctoML
Thesis: Simulating Dynamic Tensor Rematerialization

• Dynamic Tensor Rematerialization
• ML Compiler Design (TVM Relay)

Josh Pollock
BS 2020 → PhD Student at MIT
Thesis: Sidewinder: Designing Correct Program State Visualizations

• Program State Visualization
• ML Compiler Design (TVM Relay)

Taylor Blau
BS 2020 → Github
Thesis: Verifying Strong Eventual Consistency in δ-CRDTs

• PL for 3D Printing
• Also advised by Talia Ringer on Formal Verification

David Thien
BS 2019 → PhD Student at UCSD

• Floating-point Accuracy
• Mixed-precision Optimization

Jifan Zhang
BS 2019 → MS Student at UW

• ML Compiler Design (TVM Relay)
• Also advised by Kevin Jamieson on Learning Theory

Melissa Hovik
BS 2018 → MS Student and Instructor at UW

• PL for 3D Printing

Chen Qiu
BS 2018 → MS Student at UW → Facebook

• Floating-point Accuracy
• Random Numerical Testing

Justin Adsuara
BS 2018 → Hilton Hotels

• Verification of Distributed Systems Under Churn
• Formally Verified Serialization

Adam T. Geller
BS 2018 → PhD Student at UBC

• CSS Formalization in SMT
• Web Page Layout Verification

Paul Curry
BS 2018 → Xnor.ai → Apple

• PL for 3D Printing

Ryan Doenges
BS 2017 → PhD Student at Cornell

• Formal Verification of Distributed Systems Under Churn

Luke Nelson
Co-advised with Xi Wang
BS 2017 → PhD Student at UW

• Formally verified, self-hosted eBPF JIT Compilation

Miranda Edwards
BS 2017 → Cisco Meraki

• Formally Verified Distributed Systems

Keith Simmons
BS 2017 → Microsoft

• Formally Verified Distributed Systems

Steve Anton
BS 2017 → Google

• Formally Verified Distributed Systems

Seth Pendergrass
BS 2016 → Microsoft

• PL for 3D Printing

Daryl Zuniga
BS 2015 → Microsoft

• Formal Verification of Peephole Optimization in CompCert

Juliet Oh
HS 2016 → BA Student at Princeton

• PL for 3D Printing