Joined 2021
Advising and Mentoring
Current Postdoctoral Researchers
Current PhD Students
🚀
Joined 2022
🔎
Automated Numerical Accuracy Improvement
🔎
Efficient Proofs for Congruence Closure
Current Bachelors Students
🚀
Joined 2022
âž•
Co-advised with Gus Henry Smith
🔎
Hardware Software Co-design for ML Accelerators
🚀
Joined 2021
âž•
Co-advised with Gus Henry Smith
🔎
Hardware Software Co-design for ML Accelerators
🚀
Joined 2019
âž•
Co-advised with Pavel Panchekha, Bill Zorn
🔎
Optimizing Mixed-precision Numerical Accuracy
Graduated PhD Students
🎓
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
🎓
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
🎓
PhD 2021
âž•
Co-advised with Dan Grossman
🔎
Number Systems Analysis and Optimization
📜
Rounding
⮕
Numerical Hardware Architect at Intel
🎓
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
🎓
PhD 2020
🔎
ML Compiler Design (TVM Relay)
📜
Principled Optimization Of Dynamic Neural Networks
⮕
Co-founder and CTO at OctoML
🎓
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
🎓
PhD 2019
âž•
Co-advised with Michael D. Ernst, Thomas E. Anderson
🔎
Formal Verification and Interactive Visualization of Distributed Systems
📜
A Step-through Debugger for Distributed Systems
⮕
Lecturer at Brown University
🎓
PhD 2018
âž•
Co-advised with Dan Grossman
🔎
Formal Verification of Peephole Optimizations in CompCert
📜
Pushing the Limits of Compiler Verification
⮕
🎓
PhD 2018
âž•
Co-advised with Michael D. Ernst
🔎
Formal Verificaton and Analysis of Radiotherapy Control Systems
📜
Practical Verification of Safety-Critical Systems
⮕
Galois
🎓
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
⮕
⮕
Co-founder at Nexus
Graduated Masters Students
🎓
MS 2022
🔎
Congruence + Relational Databases
⮕
PhD Student at the University of Washington
🎓
MS 2020
🔎
Dynamic Tensor Rematerialization
⮕
PhD Student at the University of Utah
🎓
MS 2015
🔎
Dynamic Numerical Error Analysis
⮕
PhD Student at UC San Diego
Graduated Bachelors Students
🎓
BS 2022
âž•
Co-advised with Steven Lyubomirsky
🔎
Dynamic Tensor Rematerialization
⮕
PhD Student at Princeton University
🎓
BS 2021
🔎
Relational E-matching
📜
Relational E-matching
⮕
MS Student at the University of Washington
🎓
BS 2020
âž•
Co-advised with Talia Ringer
🔎
PL for 3D Printing
📜
Verifying Strong Eventual Consistency in δ-CRDTs
⮕
GitHub
🎓
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
🎓
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
🎓
BS 2019
âž•
Co-advised with Jared Roesch
🔎
ML Compiler Design (TVM Relay)
⮕
MS Student at the University of Washington
🎓
BS 2019
âž•
Co-advised with Jared Roesch
🔎
ML Compiler Design (TVM Relay)
⮕
MS Student at the University of Washington
🎓
BS 2019
🔎
ML Compiler Design (TVM Relay)
⮕
MS Student at the University of Washington (w/ Kevin Jamieson)
⮕
PhD Student at the University of Wisconsinn
🎓
BS 2019
âž•
Co-advised with Pavel Panchekha
🔎
Automated Numerical Accuracy Improvement
⮕
PhD Student at UCSD
🎓
BS 2018
🔎
PL for 3D Printing
⮕
MS Student and Instructor at the University of Washington
⮕
Instructor at CalTech
🎓
BS 2018
âž•
Co-advised with Doug Woos
🔎
Verification of Distributed Systems Under Churn
🔎
Formally Verified Serialization
⮕
Hilton Hotels
🎓
BS 2018
âž•
Co-advised with Pavel Panchekha
🔎
Automated Numerical Accuracy Improvement
⮕
MS Student at the University of Washington
⮕
🎓
BS 2018
âž•
Co-advised with Pavel Panchekha
🔎
CSS Formalization in SMT
🔎
Web Page Layout Verification
⮕
PhD Student at the University of British Columbia
🎓
BS 2017
âž•
Co-advised with James R. Wilcox, Doug Woos
🔎
Formally Verified Distributed Systems
⮕
🎓
BS 2017
âž•
Co-advised with James R. Wilcox, Doug Woos
🔎
Formal Verification of Distributed Systems Under Churn
⮕
PhD Student at Cornell University
🎓
BS 2017
âž•
Co-advised with James R. Wilcox
🔎
Formally Verified Distributed Systems
⮕
Cisco Meraki
🎓
BS 2017
âž•
Co-advised with Xi Wang
🔎
Formally verified
🔎
self-hosted eBPF JIT Compilation
⮕
PhD Student at the University of Washington
🎓
BS 2017
âž•
Co-advised with James R. Wilcox, Doug Woos
🔎
Formally Verified Distributed Systems
⮕
Microsoft
🎓
BS 2015
âž•
Co-advised with Eric Mullen, Dan Grossman
🔎
Formal Verification of Peephole Optimizations in CompCert
⮕
Microsoft
🎓
BS 2014
âž•
Co-advised with Pavel Panchekha
🔎
Automated Numerical Accuracy Improvement
⮕
MS Student at the University of Washington
Graduated High School Students
🎓
HS 2021
âž•
Co-advised with Josh Pollock, Eunice Jun
🔎
Program State Visualization
🔎
CS Education
⮕
BA Student at Princeton University
🎓
HS 2018
âž•
Co-advised with Chandrakana Nandi
🔎
PL for 3D Printing
⮕
BS Student at the University of Washington