Hi there! I'm Zhengyao . I'm a PhD student in CS at Carnegie Mellon University advised by Bryan Parno. I also work closely with Milijana Surbatovich.
I'm broadly interested in formal verification, and right now, I'm working on verifying compilers for spatial dataflow architectures using the Lean theorem prover.
Previously, I got my undergraduate degree in Math and Computer Science from the University of Illinois at Urbana-Champaign, where I had the honor to work with Xiaohong Chen, Grigore Roșu, Madhusudan Parthasarathy, and Vikram Adve.
Email: zhengyal at cmu.edu
CV dblp GitHub
Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
Zhengyao Lin, Yi Cai, Milijana Surbatovich
PLDI 2026
repo artifact
Towards Practical, End-to-End Formally Verified X.509 Certificate Validators with Verdict
Zhengyao Lin, Michael McLoughlin, Pratap Singh, Rory Brennan-Jones, Paul Hitchcox, Joshua Gancher, Bryan Parno
USENIX Sec 2025
paper repo artifact bibtex
Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust
Yi Cai, Pratap Singh, Zhengyao Lin, Jay Bosamiya, Joshua Gancher, Milijana Surbatovich, Bryan Parno
USENIX Sec 2025
paper repo artifact bibtex
Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Yi Zhou, Amar Shah, Zhengyao Lin, Marijn Heule, Bryan Parno
CADE 2025
paper repo bibtex
FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions
Zhengyao Lin, Joshua Gancher, Bryan Parno
OOPSLA 2024
paper repo artifact bibtex
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier
Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Roșu
OOPSLA 2023
paper repo artifact bibtex
Synthesizing Axiomatizations using Logic Learning
Paul Krogmeier*, Zhengyao Lin*, Adithya Murali*, P. Madhusudan
OOPSLA 2022
paper repo artifact bibtex
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation
Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Roșu
CAV 2021
paper repo artifact bibtex
Language-Parametric Compiler Validation with Application to LLVM
Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram Adve, Grigore Roșu
ASPLOS 2021
paper artifact bibtex