Hi there! I'm Zhengyao (pronounced "gen yao"). I'm a PhD student in Computer Science at Carnegie Mellon University advised by Professor Bryan Parno.
I'm broadly interested in formal verification. Currently, I'm trying to verify compilation towards dataflow architectures and high-level synthesis, using the Lean theorem prover.
Previously, I got my undergraduate degree in Mathematics and Computer Science from the University of Illinois at Urbana-Champaign.
Email: zhengyal at cmu.edu
[CV] [dblp] [GitHub]
Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Yi Zhou, Amar Shah, Zhengyao Lin, Marijn Heule, Bryan Parno
CADE 2025
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
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
FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions
Zhengyao Lin, Joshua Gancher, Bryan Parno
OOPSLA 2024
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier
Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Roşu
OOPSLA 2023
Synthesizing Axiomatizations using Logic Learning
Paul Krogmeier*, Zhengyao Lin*, Adithya Murali*, P. Madhusudan
OOPSLA 2022
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation
Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Roşu
CAV 2021
Language-Parametric Compiler Validation with Application to LLVM
Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram Adve, Grigore Roşu
ASPLOS 2021