Yi Zhou


Email:
yeet [at] cmu [dot] edu

Office:
2128D, CIC, 4720 Forbes Ave, Pittsburgh PA 15213

Hello there. I'm Yi (pronounced as the letter "e"). Somewhere on this page you might see a pictorial representation of me.

I'm currently a Ph.D. student at CMU, where I have the privilege to have Bryan Parno as my advisor. Prior to that, I received my B.S. and M.S. from UIUC, where I was fortunate to have Michael Bailey as my advisor.

My current research interest is mainly in verification engineering, where I investigate in ways to make formally verified software faster to develop and easier to maintain.

In my free time I enjoy playing the electric guitar and lifting weights, despite being terrible at those.

This website's template was shamelessly copied from Deepak Kumar.

Publications

Context Pruning for More Robust SMT-based Program Verification. Yi Zhou, Jay Bosamiya, Jessica Li, Marijn Heule, Bryan Parno. Formal Methods in Computer-Aided Design (FMCAD), October, 2024.

A Framework for Debugging Automated Program Verification Proofs via Proof Actions. [Distinguished Paper Award] Chanhee Cho, Yi Zhou, Jay Bosamiya, Bryan Parno. International Conference on Computer-Aided Verification (CAV), July, 2024

Galápagos: Developing Verified Low Level Cryptography on Heterogeneous Hardwares. Yi Zhou, Sydney Gibson, Sarah Cai, Menucha Winchell, Bryan Parno. ACM Conference on Computer and Communications Security (CCS), November, 2023.

Mariposa: Measuring SMT Instability in Automated Program Verification. Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn Heule, Bryan Parno. Formal Methods in Computer-Aided Design (FMCAD), October, 2023.

Verus: Verifying Rust Programs using Linear Ghost Types. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel. ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), October, 2023.

Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, Bryan Parno. USENIX Symposium on Operating Systems Design and Implementation (OSDI), July, 2023.

Linear Types for Large-Scale Systems Verification. [Distinguished Paper Award] Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, Chris Hawblitzel. ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), December, 2022.

A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. Antoine Delignat-Lavaud, Cedric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou. IEEE Symposium on Security and Privacy (S&P), May, 2021.

Erays: Reverse Engineering Ethereum's Opaque Smart Contracts. Yi Zhou, Deepak Kumar, Surya Bakshi, Joshua Mason, Andrew Miller, Michael Bailey. USENIX Security Symposium (USENIX), August, 2018.

Understanding the Mirai Botnet. Manos Antonakakis, Tim April, Michael Bailey, Matt Bernhard, Elie Bursztein, Jaime Cochran, Zakir Durumeric, J. Alex Halderman, Luca Invernizzi, Michalis Kallitsis, Deepak Kumar, Chaz Lever, Zane Ma, Joshua Mason, Damian Menscher, Chad Seaman, Nick Sullivan, Kurt Thomas, Yi Zhou. USENIX Security Symposium (USENIX), August, 2017.