
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 co-founded CertiK, a blockchain cybersecurity startup. Press on CertiK: Forbes, CACM, Cointelegraph, Coindesk.
[CV] [Bio] [Google Scholar] [Research Statement]
Hiring!
My Columbia lab is looking for Ph.D. students and Postdocs. Check out our recent S&P'21, CACM Research Highlights, SOSP'19 (Best Paper Award), PLDI'18, OSDI'16, and POPL'15 papers (and the press release) for an overview of our latest breakthrough on building trustworthy systems software.
News
March 2021 | DistAI is accepted to appear at OSDI 2021. |
March 2021 | Awarded Amazon Research Awards. |
March 2021 | Grant on Microverification of Linux OS Kernel is funded by NSF. |
February 2021 | Gleipnir is accepted to appear at PLDI 2021. |
Janurary 2021 | Named the inaugural Tang Family Assistant Professor. |
December 2020 | A follow-up work of SeKVM is accepted to appear at USENIX Security 2021. |
November 2020 | SeKVM is accepted to appear at S&P (Oakland) 2021. |
July 2020 | Received a research gift from Arm. |
March 2020 | Nominated by Columbia University for a Packard Fellowship. |
October 2019 | Serval won the best paper award at SOSP 2019. |
Education
- Ph.D. in Computer Science, Yale University, December 2016
- Advisor: Prof. Zhong Shao.
- Thesis: An Extensible Architecture for Building Certified Sequential and Concurrent OS Kernels.
- Distinguished Dissertation of Yale Graduate School of Art and Science.
- B.S. in Computer Science, Tsinghua University, June 2011.
- Rank: 4/140. Graduation with Highest Distinction (3 out of 140).
Manuscripts
-
[arXiv] SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts. S. Lin, X. Sun, J. Yao, and R. Gu
-
[arXiv] CertiQ: Contract-based Verification of a Realistic Quantum Compiler. Y. Shi, X. Li, R. Tao, A. Javadi-Abhari, A. Cross, F. Chong, and R. Gu
Select Publications
-
[PLDI 2021][New] 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] [New] A Secure and Formally Verified Linux KVM Hypervisor. S. Li, X. Li, R. Gu, J. Nieh, and J. Hui
-
[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
-
[POPL 2020] Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation. M. Liu, L. Rieg, Z. Shao, R. Gu, D. Costanzo, J. Kim, and M. Yoon
-
[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
-
[SOSP 2019] Using Concurrent Relational Logic with Helper for Verifying the AtomFS File System. M. Zou, H. Ding, D. Du, M. Fu, R. Gu, and H. Chen
-
[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
-
[PLDI 2016] End-to-End Verification of Information-Flow Security for C and Assembly Programs. D. Constanzo, Z. Shao, and R. Gu
-
[PLDI 2016] Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. H. Chen, X. Wu, Z. Shao, J. Lockerman, and R. Gu
[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
Select Awards
Amazon Research Awards, 2021. |
Named the inaugural Tang Family Assistant Professor, 2021. |
Columbia University’s Final Nominee for the Packard Fellowship, 2020. |
SOSP Best Paper Award, 2019. |
Communications of the ACM (CACM) Research Highlights, 2019. |
MIT Technology Review 35 Innovators Under 35 Semi-Finalist, 2019. |
Distinguished Dissertation Award, Yale University, 2016. |
Yale Nominee, ACM Doctoral Dissertation Award, 2016. |
Robert Willets Carle Scholarship, Yale University, 2016. |
Graduation with Highest Distinction (3 out of 140), Tsinghua University, 2011. |
Outstanding Undergraduate of Beijing City, China, 2011. |
Honors Undergraduate Thesis Award (5 out of 140), Tsinghua University, 2011. |
Program Committees
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, and Xuheng Li.
- 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 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)
