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 Mathematics and Computer Science from the University of Illinois at Urbana-Champaign.
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
Cazamariposas: Automated Instability Debugging in SMT-based Program Verification
Yi Zhou, Amar Shah, Zhengyao Lin, Marijn Heule, Bryan Parno
CADE 2025
paper repo bibtex
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
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