Deep Specifications and Certified Abstraction Layers. - Ronghui Gu; Jérémie Koenig; Tahina Ramananandro; Zhong Shao 001; Xiongnan (Newman) Wu; Shu-Chun Weng; Haozhong Zhang; Yu Guo (POPL, 2015)

CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. - Ronghui Gu; Zhong Shao 001; Hao Chen 023; Xiongnan (Newman) Wu; Jieung Kim; Vilhelm Sjöberg; David Costanzo (OSDI, 2016)

End-to-end verification of information-flow security for C and assembly programs. - David Costanzo; Zhong Shao 001; Ronghui Gu (PLDI, 2016)

Safety and Liveness of MCS Lock - Layer by Layer. - Jieung Kim; Vilhelm Sjöberg; Ronghui Gu; Zhong Shao 001 (APLAS, 2017)

An auditing language for preventing correlated failures in the cloud. - Ennan Zhai; Ruzica Piskac; Ronghui Gu; Xun Lao; Xi Wang (Proc. ACM Program. Lang., 2017)

Partial Order Aware Concurrency Sampling. - Xinhao Yuan; Junfeng Yang; Ronghui Gu (CAV (2), 2018)

Certified concurrent abstraction layers. - Ronghui Gu; Zhong Shao 001; Jieung Kim; Xiongnan (Newman) Wu; Jérémie Koenig; Vilhelm Sjöberg; Hao Chen 023; David Costanzo; Tahina Ramananandro (PLDI, 2018)

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. - Hao Chen 023; Xiongnan (Newman) Wu; Zhong Shao 001; Joshua Lockerman; Ronghui Gu (J. Autom. Reason., 2018)

Scaling symbolic evaluation for automated verification of systems code with Serval. - Luke Nelson; James Bornholt; Ronghui Gu; Andrew Baumann; Emina Torlak; Xi Wang 005 (SOSP, 2019)

Using concurrent relational logic with helpers for verifying the AtomFS file system. - Mo Zou; Haoran Ding; Dong Du 003; Ming Fu; Ronghui Gu; Haibo Chen 001 (SOSP, 2019)

Building certified concurrent OS kernels. - Ronghui Gu; Zhong Shao 001; Hao Chen 023; Jieung Kim; Jérémie Koenig; Xiongnan (Newman) Wu; Vilhelm Sjöberg; David Costanzo (Commun. ACM, 2019)

Contract-based verification of a realistic quantum compiler. - Yunong Shi; Xupeng Li; Runzhou Tao; Ali Javadi-Abhari; Andrew W. Cross; Frederic T. Chong; Ronghui Gu (CoRR, 2019)

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

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

Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. - Mengqi Liu 001; Lionel Rieg; Zhong Shao 001; Ronghui Gu; David Costanzo; Jung-Eun Kim; Man-Ki Yoon (Proc. ACM Program. Lang., 2020)

DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. - Jianan Yao; Runzhou Tao; Ronghui Gu; Jason Nieh; Suman Jana; Gabriel Ryan (OSDI, 2021)

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

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

A Secure and Formally Verified Linux KVM Hypervisor. - Shih-Wei Li; Xupeng Li; Ronghui Gu; Jason Nieh; John Zhuang Hui (SP, 2021)

Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. - Shih-Wei Li; Xupeng Li; Ronghui Gu; Jason Nieh; John Zhuang Hui (USENIX Security Symposium, 2021)

SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts. - Shaokai Lin; Xinyuan Sun; Jianan Yao; Ronghui Gu (CoRR, 2021)

Gleipnir: Toward Practical Error Analysis for Quantum Programs (Extended Version). - Runzhou Tao; Yunong Shi; Jianan Yao; John Hui; Frederic T. Chong; Ronghui Gu (CoRR, 2021)

UPGRADVISOR: Early Adopting Dependency Updates Using Hybrid Program Analysis and Hardware Tracing. - Yaniv David; Xudong Sun 019; Raphael J. Sofaer; Aditya Senthilnathan; Junfeng Yang; Zhiqiang Zuo 002; Guoqing Harry Xu; Jason Nieh; Ronghui Gu (OSDI, 2022)

Design and Verification of the Arm Confidential Compute Architecture. - Xupeng Li; Xuheng Li; Christoffer Dall; Ronghui Gu; Jason Nieh; Yousuf Sait; Gareth Stockwell (OSDI, 2022)

DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. - Jianan Yao; Runzhou Tao; Ronghui Gu; Jason Nieh (OSDI, 2022)

Giallar: push-button verification for the qiskit Quantum compiler. - Runzhou Tao; Yunong Shi; Jianan Yao; Xupeng Li; Ali Javadi-Abhari; Andrew W. Cross; Frederic T. Chong; Ronghui Gu (PLDI, 2022)

Spoq: Scaling Machine-Checkable Systems Verification in Coq. - Xupeng Li; Xuheng Li; Wei Qiang; Ronghui Gu; Jason Nieh (OSDI, 2023)

Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor. - Zhenyang Dai; Shuang Liu; Vilhelm Sjöberg; Xupeng Li; Yu Chen 004; Wenhao Wang 001; Yuekai Jia; Sean Noble Anderson; Laila Elbeheiry; Shubham Sondhi; Yu Zhang; Zhaozhong Ni; et al. (ASPLOS (2), 2024)

Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions. - Jianan Yao; Runzhou Tao; Ronghui Gu; Jason Nieh (Proc. ACM Program. Lang., 2024)

SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification. - Jieung Kim; Ronghui Gu; Zhong Shao 001 (J. Syst. Archit., 2024)

ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions. - Jieung Kim; Jérémie Koenig; Hao Chen 023; Ronghui Gu; Zhong Shao 001 (J. Syst. Archit., 2024)

Quantum Virtual Machines. - Runzhou Tao; Hongzheng Zhu; Jason Nieh; Jianan Yao; Ronghui Gu (OSDI, 2025)

Security Analysis and Formal Verification on Blockchain and its Applications. - Kang Li; Ronghui Gu; Jun Xu 019; Zhaofeng Chen; Siwei Wu; Yajin Zhou; Mu Zhang 001; Xiapu Luo; Yuzhe Tang; Yi Li; Xiaokuan Zhang; Yibo Wang 006 (Found. Trends Priv. Secur., 2025)