Towards a Trustworthy Semantics-Based Language Framework via Proof Generation.
Xiaohong Chen, Zhengyao Lin, Thai Trinh, and Grigore Roșu.
Proceedings of the 33rd International Conference on Computer-Aided Verication (CAV 2021), July 2021. [pdf]
Language-Parametric Compiler Validation with Application to LLVM.
Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram Adve, and Grigore Roșu.
Proceedings of the 26th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2021), April 2021. [pdf]
Pecan: An Automated Theorem Prover (poster).
Reed Oei, Dun Ma, Zhengyao Lin, Yikai Teng, and Pavle Vuksanovic.
MAA Student Poster Session, Joint Mathematics Meetings (JMM 2021), Jan 2021. [pdf]
Trustworthy Program Verication via Proof Generation.
Zhengyao Lin, Xiaohong Chen, Thai Trinh, John Wang, and Grigore Roșu. [preprint]
A Translation Validation Algorithm for LLVM Register Allocators.
Zhengyao Lin, Theodoros Kasampalis, and Vikram Adve.
An Interactive Theorem Prover for Matching Logic with Proof Object Generation.
Zhengyao Lin, Xiaohong Chen, and Grigore Roșu. [preprint]