Ronghui Gu

According to our database, Ronghui Gu authored at least 31 papers between 2015 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions.

Jieung Kim, Jérémie Koenig, Hao Chen, Ronghui Gu, Zhong Shao

J. Syst. Archit., February, 2024

SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification.

Jieung Kim, Ronghui Gu, Zhong Shao

J. Syst. Archit., February, 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., January, 2024

Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor.

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

Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2024

2023

Spoq: Scaling Machine-Checkable Systems Verification in Coq.

Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, Jason Nieh

Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation, 2023

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

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols.

Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh

Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, 2022

Design and Verification of the Arm Confidential Compute Architecture.

Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, Gareth Stockwell

Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, 2022

UPGRADVISOR: Early Adopting Dependency Updates Using Hybrid Program Analysis and Hardware Tracing.

Yaniv David, Xudong Sun, Raphael J. Sofaer, Aditya Senthilnathan, Junfeng Yang, Zhiqiang Zuo, Guoqing Harry Xu, Jason Nieh, Ronghui Gu

Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, 2022

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

SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts.

Shaokai Lin, Xinyuan Sun, Jianan Yao, Ronghui Gu

CoRR, 2021

Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor.

Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, John Zhuang Hui

Proceedings of the 30th USENIX Security Symposium, 2021

A Secure and Formally Verified Linux KVM Hypervisor.

Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, John Zhuang Hui

Proceedings of the 42nd IEEE Symposium on Security and Privacy, 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

Proceedings of the SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles, 2021

Gleipnir: toward practical error analysis for Quantum programs.

Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong, Ronghui Gu

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols.

Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, Gabriel Ryan

Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation, 2021

2020

Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation.

Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, Man-Ki Yoon

Proc. ACM Program. Lang., 2020

Learning nonlinear loop invariants with gated continuous logic networks.

Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, Ronghui Gu

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

CLN2INV: Learning Loop Invariants with Continuous Logic Networks.

Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, Suman Jana

Proceedings of the 8th International Conference on Learning Representations, 2020

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

Building certified concurrent OS kernels.

Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jérémie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjöberg, David Costanzo

Commun. ACM, 2019

Using concurrent relational logic with helpers for verifying the AtomFS file system.

Mo Zou, Haoran Ding, Dong Du, Ming Fu, Ronghui Gu, Haibo Chen

Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019

Scaling symbolic evaluation for automated verification of systems code with Serval.

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang

Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019

2018

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers.

Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu

J. Autom. Reason., 2018

Certified concurrent abstraction layers.

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, Tahina Ramananandro

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Partial Order Aware Concurrency Sampling.

Xinhao Yuan, Junfeng Yang, Ronghui Gu

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

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

Safety and Liveness of MCS Lock - Layer by Layer.

Jieung Kim, Vilhelm Sjöberg, Ronghui Gu, Zhong Shao

Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

2016

End-to-end verification of information-flow security for C and assembly programs.

David Costanzo, Zhong Shao, Ronghui Gu

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, David Costanzo

Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation, 2016

2015

Deep Specifications and Certified Abstraction Layers.

Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, Yu Guo

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015