Publications

Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh (2024). Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Function. POPL 2024.

PDF Code

Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui (2023). Leveraging Large Language Models for Automated Proof Synthesis in Rust. arXiv preprint arXiv:2311.03739.

Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh (2022). DuoAI: Fast, automated inference of inductive invariants for verifying distributed protocols. OSDI 2022.

PDF Code

Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, Ronghui Gu (2022). Giallar: Push-Button Verification for the Qiskit Quantum Compiler. PLDI 2022.

PDF Code

Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, Ronghui Gu (2021). Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware. SOSP 2021.

PDF Code

Shaokai Lin, Xinyuan Sun, Jianan Yao, Ronghui Gu (2021). Scivik: A versatile framework for specifying and verifying smart contracts. Memorial Volume for Shoucheng Zhang, World Scientific.

PDF

Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, Gabriel Ryan (2021). DistAI: Data-driven automated invariant learning for distributed protocols. OSDI 2021.

PDF Code

Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T Chong, Ronghui Gu (2021). Gleipnir: toward practical error analysis for Quantum programs. PLDI 2021.

PDF Code

Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, Ronghui Gu (2020). Learning nonlinear loop invariants with gated continuous logic networks. PLDI 2020.

PDF Code

Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, Suman Jana (2020). CLN2INV: Learning Loop Invariants with Continuous Logic Networks. ICLR 2020.

PDF Code