Ronghui Gu

38 papers A* 20B 1Journal 14Unranked 3
YearRankTypeTitle / Venue / Authors
2026 — conf
Highly Automated Verification of Security Properties for Unmodified System Software.
ASPLOS (2)
Ganxiang Yang, Wei Qiang, Yi Rong, Xuheng Li, Fanqi Yu, Jason Nieh, Ronghui Gu
2025 A* conf
Quantum Virtual Machines.
OSDI
Runzhou Tao, Hongzheng Zhu, Jason Nieh, Jianan Yao, Ronghui Gu
2025 J jnl
Security Analysis and Formal Verification on Blockchain and its Applications.
Found. Trends Priv. Secur.
Kang Li, Ronghui Gu, Jun Xu, Zhaofeng Chen, Siwei Wu, Yajin Zhou, Mu Zhang, Xiapu Luo, Yuzhe Tang, Yi Li, Xiaokuan Zhang, Yibo Wang
2024 J jnl
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions.
Proc. ACM Program. Lang.
Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh
2024 J jnl
SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification.
J. Syst. Archit.
Jieung Kim, Ronghui Gu, Zhong Shao
2024 J jnl
ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions.
J. Syst. Archit.
Jieung Kim, Jérémie Koenig, Hao Chen, Ronghui Gu, Zhong Shao
2024 — conf
Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor.
ASPLOS (2)
Zhenyang Dai, Shuang Liu, Vilhelm Sjöberg, Xupeng Li, Yu Chen, Wenhao Wang, Yuekai Jia, Sean Noble Anderson, Laila Elbeheiry, Shubham Sondhi, Yu Zhang, Zhaozhong Ni, Shoumeng Yan, Ronghui Gu, Zhengyu He
2023 A* conf
Spoq: Scaling Machine-Checkable Systems Verification in Coq.
OSDI
Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, Jason Nieh
2022 A* conf
Design and Verification of the Arm Confidential Compute Architecture.
OSDI
Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, Gareth Stockwell
2022 A* conf
DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols.
OSDI
Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh
2022 J jnl
Giallar: Push-Button Verification for the Qiskit Quantum Compiler.
CoRR
Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, Ronghui Gu
2022 A* conf
Giallar: push-button verification for the qiskit Quantum compiler.
PLDI
Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, Ronghui Gu
2022 A* conf
UPGRADVISOR: Early Adopting Dependency Updates Using Hybrid Program Analysis and Hardware Tracing.
OSDI
Yaniv David, Xudong Sun, Raphael J. Sofaer, Aditya Senthilnathan, Junfeng Yang, Zhiqiang Zuo, Guoqing Harry Xu, Jason Nieh, Ronghui Gu
2021 A* conf
A Secure and Formally Verified Linux KVM Hypervisor.
SP
Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, John Zhuang Hui
2021 A* conf
DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols.
OSDI
Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, Gabriel Ryan
2021 A* conf
Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware.
SOSP
Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, Ronghui Gu
2021 A* conf
Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor.
USENIX Security Symposium
Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, John Zhuang Hui
2021 J jnl
Gleipnir: Toward Practical Error Analysis for Quantum Programs (Extended Version).
CoRR
Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong, Ronghui Gu
2021 A* conf
Gleipnir: toward practical error analysis for Quantum programs.
PLDI
Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong, Ronghui Gu
2021 J jnl
SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts.
CoRR
Shaokai Lin, Xinyuan Sun, Jianan Yao, Ronghui Gu
2020 A* conf
CLN2INV: Learning Loop Invariants with Continuous Logic Networks.
ICLR
Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, Suman Jana
2020 J jnl
Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks.
CoRR
Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, Ronghui Gu
2020 A* conf
Learning nonlinear loop invariants with gated continuous logic networks.
PLDI
Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, Ronghui Gu
2020 J jnl
Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation.
Proc. ACM Program. Lang.
Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, Man-Ki Yoon
2019 J jnl
Building certified concurrent OS kernels.
Commun. ACM
Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jérémie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjöberg, David Costanzo
2019 J jnl
CLN2INV: Learning Loop Invariants with Continuous Logic Networks.
CoRR
Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, Suman Jana
2019 J jnl
Contract-based verification of a realistic quantum compiler.
CoRR
Yunong Shi, Xupeng Li, Runzhou Tao, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, Ronghui Gu
2019 A* conf
Scaling symbolic evaluation for automated verification of systems code with Serval.
SOSP
Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang
2019 A* conf
Using concurrent relational logic with helpers for verifying the AtomFS file system.
SOSP
Mo Zou, Haoran Ding, Dong Du, Ming Fu, Ronghui Gu, Haibo Chen
2018 A* conf
Certified concurrent abstraction layers.
PLDI
Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, Tahina Ramananandro
2018 — conf
Partial Order Aware Concurrency Sampling.
CAV (2)
Xinhao Yuan, Junfeng Yang, Ronghui Gu
2018 J jnl
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers.
J. Autom. Reason.
Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu
2017 J jnl
An auditing language for preventing correlated failures in the cloud.
Proc. ACM Program. Lang.
Ennan Zhai, Ruzica Piskac, Ronghui Gu, Xun Lao, Xi Wang
2017 B conf
Safety and Liveness of MCS Lock - Layer by Layer.
APLAS
Jieung Kim, Vilhelm Sjöberg, Ronghui Gu, Zhong Shao
2016 A* conf
CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.
OSDI
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, David Costanzo
2016 A* conf
End-to-end verification of information-flow security for C and assembly programs.
PLDI
David Costanzo, Zhong Shao, Ronghui Gu
2016 A* conf
Toward compositional verification of interruptible OS kernels and device drivers.
PLDI
Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu
2015 A* conf
Deep Specifications and Certified Abstraction Layers.
POPL
Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, Yu Guo