Students

PhD

Amy Zhu

Amy Zhu
Co-advised with Adriana Schulz
Joined Summer 2020

  • Rewrite Synthesis
  • PL for Knitting

Gus Smith

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

Steven Lyubomirsky
Joined Autumn 2016

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

Chandrakana Nandi

Chandrakana Nandi
Co-advised with Dan Grossman
Joined Autumn 2015

  • Rewrite Synthesis
  • PL for 3D Printing and Carpentry

Jared Roesch

Jared Roesch
Joined Autumn 2015

  • ML Compiler Design (TVM Relay)
  • OctoML

Bill Zorn

Bill Zorn
Co-advised with Dan Grossman
Joined Autumn 2014

  • Floating-point Accuracy
  • Number Systems Analysis Tools

Undergraduate

Andrew Liu

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

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

  • Floating-point Accuracy
  • Mixed-precision Optimization

Mike He

Mike He
Co-advised with Steven Lyubomirsky
Joined Winter 2019

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

Adam Anderson

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

  • Rewrite Synthesis
  • PL for 3D Printing

High School

Grace Oh

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

  • Program State Visualization
  • CS Education

 

Graduated Students

PhD

Pavel Panchekha

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

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

James Wilcox

James R. Wilcox
ABD 2019 → CTO at Certora

  • Formal Verification of Distributed Systems
  • Automatic Inductive Invariant Inference

Doug Woos

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

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

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

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

Masters

Marisa Kirisame

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

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

Logan Weber

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

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

Alex Sanchez-Stern

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

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

Undergraduate

Altan Haan

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

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

Josh Pollock

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

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

David Thien
BS 2019 → PhD Student at UCSD

  • Floating-point Accuracy
  • Mixed-precision Optimization

Jifan Zhang

Jifan Zhang
BS 2019 → MS Student at UW

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

Melissa Hovik

Melissa Hovik
BS 2018 → MS Student and Instructor at UW

  • PL for 3D Printing

Chen Qiu

Chen Qiu
BS 2018 → MS Student at UW → Facebook

  • Floating-point Accuracy
  • Random Numerical Testing

Justin Adsuara

Justin Adsuara
BS 2018 → Hilton Hotels

  • Verification of Distributed Systems Under Churn
  • Formally Verified Serialization

Adam T. Geller

Adam T. Geller
BS 2018 → PhD Student at UBC

  • CSS Formalization in SMT
  • Web Page Layout Verification

Paul Curry

Paul Curry
BS 2018 → Xnor.ai → Apple

  • PL for 3D Printing

Ryan Doenges

Ryan Doenges
BS 2017 → PhD Student at Cornell

  • Formal Verification of Distributed Systems Under Churn

Luke Nelson

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

  • Formally verified, self-hosted eBPF JIT Compilation

Miranda Edwards

Miranda Edwards
BS 2017 → Cisco Meraki

  • Formally Verified Distributed Systems

Keith Simmons

Keith Simmons
BS 2017 → Microsoft

  • Formally Verified Distributed Systems

Steve Anton

Steve Anton
BS 2017 → Google

  • Formally Verified Distributed Systems

Seth Pendergrass

Seth Pendergrass
BS 2016 → Microsoft

  • PL for 3D Printing

Daryl Zuniga

Daryl Zuniga
BS 2015 → Microsoft

  • Formal Verification of Peephole Optimization in CompCert

High School

Juliet Oh

Juliet Oh
HS 2016 → BA Student at Princeton

  • PL for 3D Printing