Mike He


I am a 3rd-year Ph.D. at the Department of Computer Science, Princeton University advised by Prof. Aarti Gupta. I also obtained a M.A. in Computer Science from Princeton University. Before joining Princeton, I received my B.S. in Computer Science from the University of Washington. I was fortunate to work with Prof. Zachary Tatlock on formal methods, machine learning systems and equality saturation. My research focuses on building accessible tools for enabling practical formal methods on real-world systems. Specifically, I am working on verification infrastructures for distributed systems.

CV Mail Twitter Scholar Github LinkedIn

Profile picture

Publications & Workshops

(*: Equal contribution)

Project image
Improving Term Extraction with Acyclic Constraints
Mike He, Haichen Dong, Sharad Malik, Aarti Gupta
E-Graph Research, Applications, Practices, and Human-factors Symposium (EGRAPHS'23), 2023
Project PagePaperCode
@InProceedings{he23extraction, 
	author = {Mike He and Haichen Dong and Sharad Malik and Aarti Gupta}, 
	title = {Improving Term Extraction with Acyclic Constraints}, 
	booktitle = {E-Graph Research, Applications, Practices, and Human-factors Symposium (EGRAPHS'23)}, 
	year = {2023}, 
}
Project image
Application-Level Validation of Accelerator Designs Using a Formal Software/Hardware Interface
Bo-Yuan Huang*, Steven Lyubomirsky*, Yi Li, Mike He, Thierry Tambe, Gus Smith, Akash Gaonkar, Vishal Canumalla, Gu-Yeon Wei, Aarti Gupta, Sharad Malik, Zachary Tatlock
ACM Trans. Des. Autom. Electron. Syst., 2023
Project PagePaper
@InProceedings{huang233la, 
	author = {Bo-Yuan Huang* and Steven Lyubomirsky* and Yi Li and Mike He and Thierry Tambe and Gus Smith and Akash Gaonkar and Vishal Canumalla and Gu-Yeon Wei and Aarti Gupta and Sharad Malik and Zachary Tatlock}, 
	title = {Application-Level Validation of Accelerator Designs Using a Formal Software/Hardware Interface}, 
	booktitle = {ACM Trans. Des. Autom. Electron. Syst.}, 
	year = {2023}, 
}
Project image
From DSLs to Accelerator-rich Platform Implementations: Addressing the Mapping Gap
Bo-Yuan Huang*, Steven Lyubomirsky*, Thierry Tambe*, Yi Li, Mike He, Gus Smith, Gu-Yeon Wei, Aarti Gupta, Sharad Malik, Zachary Tatlock
Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE'21), 2021
Project PagePaperPoster
@InProceedings{huang21latte, 
	author = {Bo-Yuan Huang* and Steven Lyubomirsky* and Thierry Tambe* and Yi Li and Mike He and Gus Smith and Gu-Yeon Wei and Aarti Gupta and Sharad Malik and Zachary Tatlock}, 
	title = {From DSLs to Accelerator-rich Platform Implementations: Addressing the Mapping Gap}, 
	booktitle = {Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE'21)}, 
	year = {2021}, 
}
Project image
Dynamic Tensor Rematerialization (Spotlight)
Marisa Kirisame*, Steven Lyubomirsky*, Altan Haan*, Jennifer Brennan, Mike He, Jared Roesch, Tianqi Chen, Zachary Tatlock
International Conference on Learning Representations (ICLR'21), 2021
Project PagePaperCode
@InProceedings{kirisame2021dynamic, 
	author = {Marisa Kirisame* and Steven Lyubomirsky* and Altan Haan* and Jennifer Brennan and Mike He and Jared Roesch and Tianqi Chen and Zachary Tatlock}, 
	title = {Dynamic Tensor Rematerialization}, 
	booktitle = {International Conference on Learning Representations (ICLR'21)}, 
	year = {2021}, 
}

Experience

Amazon Web Services, May 2024 → Aug 2024
Applied Scientist Intern
Mentor: Dr. Ankush Desai
Santa Clara, CA
Taichi Graphics (Now Meshy.AI), June 2022 → Sep 2022
Compiler R&D Intern
Mentor: Zhanlue Yang, Yi Xu
Remote and Beijing, China
Strategic CAD Lab (Intel Labs), Mar 2022 → June 2022
Formal Verification Research Intern
Mentor: Dr. Zhenkun Yang
Remote and Hillsboro, OR
Programming Language and Software Engineering Lab, Oct 2019 → June 2022
Research Assistant
Mentor: Dr. Steven Lybomirsky
Seattle, WA

Talks

Project image
Ph.D. General Examination
Princeton University, April 16, 2024
Slides
Project image
CatsTail: Packet programs synthesis via Equality Saturation
Princeton University, December 2023
Slides
Project image
Improving Term Extraction with Acyclic Constraints
PLDI EGRAPHS'23, June 2023
Slides / Recording
Project image
Towards automated super-optimization for Taichi using Equality Saturation
Taichi Graphics, January 2023
Slides / Recording
Project image
Efficient E-Graph Extraction via Linear Programming
Princeton University, December 2022
Slides
Project image
Pyrope: towards correct-by-construction hardware modeling in Python/HeteroCL
Intel Labs, June 2022
Slides
Project image
Correct & Flexible Compiler Support for Custom Accelerators
SRC ADA Center, September 2021
Slides

Professional Activities

  • Artifact Evaluation Committee: POPL'25, PLDI'24, POPL'24, MLSys'23, MICRO'21
  • External Reviewer: OOPSLA'24

Misc

  • I love classical music and enjoy playing the violin. I've been playing the violin for about 20 years. I received the Lv.9 certification issued by the Central Conservatory of Music when I was in middle school. Here is a sample recording (Meditation from Thais) made in Dec. 2023. Some other recordings are available @ Bilibili (the website is in Chinese).
  • I was a part-time translator / proofreading editor in Gawr Gura's Chinese fansub team. Gura is a virtual streamer at YouTube affiliated with Hololive Production (EN).
  • My ErdÅ‘s number is 4

Friends and Colleagues (by alphabetical order of last names)


Visitors are welcomed!

This website is adapted from a template generously provided by Michael Niemeyer.