Ronghui Gu

Publication Activity (10 Years)

Years Active: 2015-2024
Publications (10 Years): 34

Top Topics

Formal Verification

Abstraction Layer

Top Venues

Publications

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