| 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 | 421* | 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 | 266 | 2015 |
| 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 | 131 | 2019 |
| End-to-End Verification of Information-Flow Security for C and Assembly Programs D Costanzo, Z Shao, R Gu PLDI 2016, 648-664, 2016 | 110 | 2016 |
| 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 | 109* | 2018 |
| 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 | 96* | 2016 |
| 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 | 80 | 2022 |
| 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 | 72 | 2021 |
| CLN2INV: Learning Loop Invariants with Continuous Logic Networks G Ryan, J Wong, J Yao, R Gu, S Jana ICLR 2020, 2020 | 59 | 2020 |
| 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 | 56* | 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 | 54 | 2020 |
| 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 | 51 | 2021 |
| 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 | 47 | 2019 |
| Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor SW Li, X Li, R Gu, J Nieh, JZ Hui USENIX Security 2021, 2021 | 41 | 2021 |
| 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 | 39* | 2019 |
| 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 | 34 | 2021 |
| Safety and Liveness of MCS Lock—Layer by Layer J Kim, V Sjöberg, R Gu, Z Shao APLAS 2017, 273-297, 2017 | 34 | 2017 |
| DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols J Yao, R Tao, R Gu, J Nieh OSDI 2022, 485-501, 2022 | 28 | 2022 |
| 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 | 26 | 2020 |
| Partial Order Aware Concurrency Sampling X Yuan, J Yang, R Gu CAV 2018, 317-335, 2018 | 23 | 2018 |
Zhong ShaoYale UniversityVerified email at yale.edu
