Language-parametric compiler validation with application to LLVM. - Theodoros Kasampalis; Daejun Park 001; Zhengyao Lin; Vikram S. Adve; Grigore Rosu (ASPLOS, 2021)

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. - Xiaohong Chen 002; Zhengyao Lin; Minh-Thai Trinh; Grigore Rosu (CAV (2), 2021)

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. - Xiaohong Chen 002; Zhengyao Lin; Minh-Thai Trinh; Grigore Rosu (Zenodo, 2021)

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. - Xiaohong Chen 002; Zhengyao Lin; Minh-Thai Trinh; Grigore Rosu (Zenodo, 2021)

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. - Xiaohong Chen 002; Zhengyao Lin; Minh-Thai Trinh; Grigore Rosu (Zenodo, 2021)

Synthesizing axiomatizations using logic learning. - Paul Krogmeier; Zhengyao Lin; Adithya Murali; P. Madhusudan (Proc. ACM Program. Lang., 2022)

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. - Zhengyao Lin; Xiaohong Chen 002; Minh-Thai Trinh; John Wang; Grigore Rosu (Zenodo, 2022)

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. - Zhengyao Lin; Xiaohong Chen 002; Minh-Thai Trinh; John Wang; Grigore Rosu (Zenodo, 2022)

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. - Zhengyao Lin; Xiaohong Chen 002; Minh-Thai Trinh; John Wang; Grigore Rosu (Zenodo, 2022)

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. - Zhengyao Lin; Xiaohong Chen 002; Minh-Thai Trinh; John Wang; Grigore Rosu (Zenodo, 2022)

WaveCert: Formal Compiler Validation for Asynchronous Dataflow Programs. - Zhengyao Lin; Joshua Gancher; Bryan Parno (CoRR, 2023)

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. - Zhengyao Lin; Xiaohong Chen 002; Minh-Thai Trinh; John Wang; Grigore Rosu (Proc. ACM Program. Lang., 2023)

FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions. - Zhengyao Lin; Joshua Gancher; Bryan Parno (Proc. ACM Program. Lang., 2024)

Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification. - Yi Zhou 025; Amar Shah; Zhengyao Lin; Marijn Heule; Bryan Parno (CADE, 2025)