Ikuti
Ronghui Gu
Ronghui Gu
Associate Professor of Computer Science, Columbia University
Email yang diverifikasi di columbia.edu - Beranda
Judul
Dikutip oleh
Dikutip oleh
Tahun
CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels
R Gu, Z Shao, H Chen, XN Wu, J Kim, V Sjöberg, D Costanzo
OSDI 2016, 653-669, 2016
443*2016
Deep Specifications and Certified Abstraction Layers
R Gu, J Koenig, T Ramananandro, Z Shao, XN Wu, SC Weng, H Zhang, ...
POPL 2015, 595-608, 2015
2762015
Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval
L Nelson, J Bornholt, R Gu, A Baumann, E Torlak, X Wang
SOSP 2019, 225-242, 2019
1452019
Certified Concurrent Abstraction Layers
R Gu, Z Shao, J Kim, XN Wu, J Koenig, V Sjöberg, H Chen, D Costanzo, ...
PLDI 2018, 646-661, 2018
116*2018
End-to-End Verification of Information-Flow Security for C and Assembly Programs
D Costanzo, Z Shao, R Gu
PLDI 2016, 648-664, 2016
1132016
Design and Verification of the Arm Confidential Compute Architecture
X Li, X Li, C Dall, R Gu, J Nieh, Y Sait, G Stockwell
OSDI 2022, 465-484, 2022
1022022
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
H Chen, XN Wu, Z Shao, J Lockerman, R Gu
PLDI 2016, 431-447, 2016
98*2016
A Secure and Formally Verified Linux KVM Hypervisor
SW Li, X Li, R Gu, J Nieh, JZ Hui
S&P (Oakland) 2021 1, 839-856, 2021
782021
CLN2INV: Learning Loop Invariants with Continuous Logic Networks
G Ryan, J Wong, J Yao, R Gu, S Jana
ICLR 2020, 2020
662020
Giallar: Push-button Verification for the Qiskit Quantum Compiler
R Tao, Y Shi, J Yao, X Li, A Javadi-Abhari, AW Cross, FT Chong, R Gu
PLDI 2022, 641-656, 2022
62*2022
Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks
J Yao, G Ryan, J Wong, S Jana, R Gu
PLDI 2020, 106-120, 2020
622020
DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols
J Yao, R Tao, R Gu, J Nieh, S Jana, G Ryan
OSDI 2021, 405-421, 2021
612021
Using Concurrent Relational Logic with Helpers for Verifying the AtomFS File System
M Zou, H Ding, D Du, M Fu, R Gu, H Chen
SOSP 2019, 259-274, 2019
502019
Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor
SW Li, X Li, R Gu, J Nieh, JZ Hui
USENIX Security 2021, 2021
442021
Building Certified Concurrent OS Kernels
R Gu, Z Shao, H Chen, J Kim, J Koenig, XN Wu, V Sjöberg, D Costanzo
Communications of ACM (CACM) 62 (10), 89-99, 2019
402019
DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols
J Yao, R Tao, R Gu, J Nieh
OSDI 2022, 485-501, 2022
362022
Safety and Liveness of MCS Lock—Layer by Layer
J Kim, V Sjöberg, R Gu, Z Shao
APLAS 2017, 273-297, 2017
362017
Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware
R Tao, J Yao, X Li, SW Li, J Nieh, R Gu
SOSP 2021, 866-881, 2021
352021
Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers With Temporal Isolation
M Liu, L Rieg, Z Shao, R Gu, D Costanzo, JE Kim, MK Yoon
PACMPL (POPL 2020) 4 (20), 31, 2020
272020
Partial Order Aware Concurrency Sampling
X Yuan, J Yang, R Gu
CAV 2018, 317-335, 2018
262018
Sistem tidak dapat melakukan operasi ini. Coba lagi nanti.
Artikel 1–20