@inproceedings{cazamariposas,
  author = {Zhou, Yi and Shah, Amar and Lin, Zhengyao and Heule, Marijn and Parno, Bryan},
  title = {{Cazamariposas}: Automated Instability Debugging in {SMT}-Based Program Verification},
  year = {2025},
  isbn = {978-3-031-99983-3},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  url = {https://doi.org/10.1007/978-3-031-99984-0_5},
  doi = {10.1007/978-3-031-99984-0_5},
  booktitle = {Automated Deduction -- CADE 30: 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings},
  pages = {75--94},
  numpages = {20},
  location = {Stuttgart, Germany}
}

@inproceedings{verdict,
  author = {Lin, Zhengyao and McLoughlin, Michael and Singh, Pratap and Brennan-Jones, Rory and Hitchcox, Paul and Gancher, Joshua and Parno, Bryan},
  title = {Towards Practical, End-to-End Formally Verified {X.509} Certificate Validators with {Verdict}},
  year = {2025},
  isbn = {978-1-939133-52-6},
  publisher = {USENIX Association},
  address = {USA},
  booktitle = {Proceedings of the 34th USENIX Conference on Security Symposium},
  articleno = {259},
  numpages = {17},
  location = {Seattle, WA, USA},
  series = {SEC '25}
}

@inproceedings{vest,
  author = {Cai, Yi and Singh, Pratap and Lin, Zhengyao and Bosamiya, Jay and Gancher, Joshua and Surbatovich, Milijana and Parno, Bryan},
  title = {{Vest}: Verified, Secure, High-Performance Parsing and Serialization for {Rust}},
  year = {2025},
  isbn = {978-1-939133-52-6},
  publisher = {USENIX Association},
  address = {USA},
  booktitle = {Proceedings of the 34th USENIX Conference on Security Symposium},
  articleno = {355},
  numpages = {19},
  location = {Seattle, WA, USA},
  series = {SEC '25}
}

@article{flowcert,
  author = {Lin, Zhengyao and Gancher, Joshua and Parno, Bryan},
  title = {{FlowCert}: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions},
  year = {2024},
  issue_date = {October 2024},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {8},
  number = {OOPSLA2},
  url = {https://doi.org/10.1145/3689729},
  doi = {10.1145/3689729},
  journal = {Proc. ACM Program. Lang.},
  month = oct,
  articleno = {289},
  numpages = {28}
}

@article{kprove-proof-gen,
  author = {Lin, Zhengyao and Chen, Xiaohong and Trinh, Minh-Thai and Wang, John and Ro\c{s}u, Grigore},
  title = {Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier},
  year = {2023},
  issue_date = {April 2023},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {7},
  number = {OOPSLA1},
  url = {https://doi.org/10.1145/3586029},
  doi = {10.1145/3586029},
  month = apr,
  articleno = {77},
  numpages = {29}
}

@article{axiom-synthesis,
  author = {Krogmeier, Paul and Lin, Zhengyao and Murali, Adithya and Madhusudan, P.},
  title = {Synthesizing Axiomatizations Using Logic Learning},
  year = {2022},
  issue_date = {October 2022},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {6},
  number = {OOPSLA2},
  url = {https://doi.org/10.1145/3563348},
  doi = {10.1145/3563348},
  journal = {Proc. ACM Program. Lang.},
  month = oct,
  articleno = {185},
  numpages = {29}
}

@inproceedings{krun-proof-gen,
  author = {Chen, Xiaohong and Lin, Zhengyao and Trinh, Minh-Thai and Ro\c{s}u, Grigore},
  title = {Towards a Trustworthy Semantics-Based Language Framework via Proof Generation},
  year = {2021},
  isbn = {978-3-030-81687-2},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  url = {https://doi.org/10.1007/978-3-030-81688-9_23},
  doi = {10.1007/978-3-030-81688-9_23},
  booktitle = {Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20--23, 2021, Proceedings, Part II},
  pages = {477--499},
  numpages = {23}
}

@inproceedings{keq,
  author = {Kasampalis, Theodoros and Park, Daejun and Lin, Zhengyao and Adve, Vikram S. and Ro\c{s}u, Grigore},
  title = {Language-Parametric Compiler Validation with Application to {LLVM}},
  year = {2021},
  isbn = {9781450383172},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3445814.3446751},
  doi = {10.1145/3445814.3446751},
  booktitle = {Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems},
  pages = {1004--1019},
  numpages = {16},
  location = {Virtual, USA},
  series = {ASPLOS '21}
}

@article{wavelet,
  author = {Lin, Zhengyao and Cai, Yi and Surbatovich, Milijana},
  title = {Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow},
  year = {2026},
  issue_date = {June 2026},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {10},
  number = {PLDI},
  url = {https://doi.org/10.1145/3808263},
  doi = {10.1145/3808263},
  journal = {Proc. ACM Program. Lang.},
  month = jun,
  articleno = {185},
  numpages = {25}
}