
I am the Tang Family Assistant Professor of Computer Science at Columbia University.
My research spans a range of areas in Programming Languages, Operating Systems, and Blockchain, with a focus on systems verification and proof automation.
I also co-founded CertiK, a Web3 cybersecurity unicorn startup valued at $2 billion and backed by Insight Partners, Tiger Global, Sequoia, Coatue, and Goldman Sachs. Press on CertiK: The Wall Street Jounrnal, CNBC, Bloomberg, Forbes, Yahoo Finance.
[CV] [Bio] [Google Scholar] [Research Statement]
Hiring!
My Columbia lab is looking for Ph.D. students and Postdocs. Check out our recent OSDI'22, PLDI'22, SOSP'21, OSDI'21 (best paper award), S&P'21, and CACM Research Highlights (and the press release) for an overview of our latest breakthrough on building certified systems software.
News
May 2022 | CertiK is selected as a World Economic Forum Global Innovator (class of 2022). |
April 2022 | Awarded Amazon Research Awards. |
April 2022 | CertiK closed the $88M series B3 round at $2 Billion valuation. |
March 2022 | Three papers are accepted to appear at OSDI 2022. |
February 2022 | Giallar is accepted to appear at PLDI 2022. |
November 2021 | CertiK closed the $80M series B2 round at nearly $1 Billion valuation. |
August 2021 | VRM is accepted to appear at SOSP 2021. |
July 2021 | Awarded Amazon Research Awards (co-PI). |
July 2021 | DistAI won the Jay Lepreau Best Paper Award at OSDI 2021. |
June 2021 | Selected as The Top 100 Yale Alumni In Technology Of 2021. |
April 2021 | Grant on Verified Enclave Layers ($4,563,980) is funded by DARPA. |
March 2021 | Awarded Amazon Research Awards. |
Education
- Ph.D. in Computer Science, Yale University, December 2016
- Advisor: Prof. Zhong Shao.
- Distinguished Dissertation of Yale Graduate School of Art and Science.
- B.S. in Computer Science, Tsinghua University, June 2011.
- Graduation with Highest Distinction (3 out of 140).
Selected Publications
-
[New][OSDI 2022] DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. J. Yao, R. Tao, R. Gu, and J. Nieh
-
[New][OSDI 2022] Design and Verification of the Arm Confidential Compute Architecture. X. Li, X. Li, C. Dall, R. Gu, J. Nieh, Y. Sait, and G. Stockwell
-
[New][PLDI 2022] Giallar: Push-button Verification for the Qiskit Quantum Compiler R. Tao, Y. Shi, J. Yao, X. Li, A. Javadi-Abhari, A. Cross, F. Chong, and R. Gu
-
[SOSP 2021] Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware. R. Tao, J. Yao, X. Li, Shih-Wei Li, J. Nieh, and R. Gu
-
[USENIX Security 2021] Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. S. Li, X. Li, R. Gu, J. Nieh, and J. Hui
-
[OSDI 2021] DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. J. Yao, R. Tao, R. Gu, J. Nieh, S. Jana, and G. Ryan. OSDI Jay Lepreau Best Paper Award
-
[PLDI 2021] Gleipnir: Toward Practical Error Analysis for Quantum Programs. R. Tao, Y. Shi, J. Yao, J. Hui, F. Chong, and R. Gu
-
[S&P (Oakland) 2021] A Secure and Formally Verified Linux KVM Hypervisor. S. Li, X. Li, R. Gu, J. Nieh, and J. Hui Media coverage: Columbia Engineering News
-
[PLDI 2020] Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks. J. Yao, G. Ryan, J. Wong, S. Jana, and R. Gu
-
[ICLR 2020] CLN2INV: Learning Loop Invariants with Continuous Logic Networks. G. Ryan, J. Wong, J. Yao, R. Gu, and S. Jana
-
[CACM] Building Certified Concurrent OS Kernels. R. Gu, Z. Shao, H. Chen, J. Kim, J. Koenig, X. Wu, V. Sjoberg, and D. Constanzo. Research Highlights See "Technical Perspective: The Scalability of CertiKOS" by Andrew W. Appel.
-
[SOSP 2019] Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval. L. Nelson, J. Bornholt, R. Gu, A. Baumann, E. Torlak, and X. Wang SOSP Best Paper Award
-
[PLDI 2018] Certified Concurrent Abstraction Layers. R. Gu, Z. Shao, J. Kim, X. Wu, J. Koenig, V. Sjoberg, H. Chen, D. Constanzo, and T.Ramananandro
-
[OSDI 2016] CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. R. Gu, Z. Shao, H. Chen, X. Wu, J. Kim, V. Sjoberg, and D. Constanzo Media coverage: Yale News, International Business Times, Yale Daily News
[POPL 2015] Deep Specifications and Certified Abstraction Layers. R. Gu, J. Koenig, T. Ramananandro, Z. Shao, X. Wu, S. Weng, H. Zhang, and Y. Guo
Selected Awards
Amazon Research Awards, April 2022. |
Amazon Research Awards (co-PI), July 2021. |
OSDI Jay Lepreau Best Paper Award, July 2021. |
The Top 100 Yale Alumni In Technology Of 2021, June 2021. |
Amazon Research Awards, April 2021. |
Named the inaugural Tang Family Assistant Professor, Janurary 2021. |
Columbia University’s Final Nominee for the Packard Fellowship, March 2020. |
SOSP Best Paper Award, October 2019. |
Communications of the ACM (CACM) Research Highlights, October 2019. |
Distinguished Dissertation Award, Yale University, December 2016. |
Program Committees
PLDI 2022 | ASPLOS 2022 ERC | POPL 2022 | OSDI 2021 | PLDI 2020 |
SecDev 2020 | NSDI 2019 | SoCC 2019 | SecDev 2019 | CoqPL 2019 |
PLDI 2018 ERC | SecDev 2018 | ICFP 2018 SRC |
Students
- PhD: Runzhou Tao, Jianan Yao, Xupeng Li, Xuheng Li, and Raphael Sofaer.
- Student collaborators: Shih-Wei Li, John Hui, Yunong Shi (UChicago), Gabriel Ryan, Mengqi Liu (Yale), and Xinhao Yuan.
- BS: Justin Wong, River Dillon Keefer, Jerry Lin, and Amanda Liu.
Teaching
- COMS 4115 Programming Languages and Translators (Spring 2022).
- COMS E6998 Formal Verification of System Software (Fall 2021).
- Blockchain Cyberdefense Design Challenge (Summer 2021).
- COMS E6998 Formal Verification of System Software (Fall 2020).
- COMS 4115 Programming Languages and Translators (Spring 2020).
- COMS E6998 Formal Verification of System Software (Fall 2019).
- COMS 4115 Programming Languages and Translators (Spring 2019).
- COMS E6998 Formal Verification of System Software (Fall 2018).
- COMS W3101 Programming Languages (Spring 2018).
- Graduate Seminar on Systems.

Office
515 CSB, Columbia University
Phone
+1 (212) 939-7111
CertiKOS Video (for CACM)
CertiKOS Layers (for fun)
