I am an Assistant Professor of Computer Science at Columbia University.
My research interests span a range of areas in Programming Languages, Operating Systems, and Blockchain Systems, with a focus on language-based support for safety and security, certified system software, certified programming and compilation, formal methods, and concurrency reasoning.
I am also a co-founder of CertiK, a formal verification startup. Press on CertiK: Forbes, Coindesk, Yale News.
Hiring!
My research group at Columbia University is looking for Ph.D./Master students, Postdocs, and Undergraduate interns. Check out our recent PLDI'18, OSDI'16, and POPL'15 CertiKOS papers (and the press release) for an overview of our latest breakthrough on building bug-free and hacker-resistant OS kernels. If you know both systems and programming languages, and are interested in building certified systems, send me an email.
Education
- Aug. 2011 to Aug. 2016, Yale University, Ph.D. in Computer Science.
- Advisor: Professor Zhong Shao
- Thesis: An Extensible Architecture for Building Certified Sequential and Concurrent OS Kernels.
- Distinction Dissertation of Yale Graduate School of Art and Science
- Nomination for ACM Dissertation Award
- Aug. 2007 to Jul. 2011, Tsinghua University, B.S. in Computer Science.
- Rank: 4/140
- Outstanding Undergraduate of Tsinghua University, 67 among 3500
- Honors Undergraduate Thesis of Tsinghua University, 5 among 140
Selected Conference Publications
-
[PLDI 2018] Certified Concurrent Abstraction Layers.
R. Gu, Z. Shao, J. Kim, X. Wu, J. Koenig, V. Sjoberg, C. Hao, D. Constanzo, and T.Ramananandro
-
[OOPSLA 2017] An Auditing Language for Preventing Correlated Failures in the Cloud.
E. Zhai, R. Piskac, R. Gu, X. Lao, and X. Wang
-
[OSDI 2016] CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.
R. Gu, Z. Shao, C. Hao, X. Wu, J. Kim, V. Sjoberg, and D. Constanzo
Media coverage: Yale News, International Business Times, Yale Daily News
Honor: Selected in the Research Highlights section of the CACM.
-
[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.
[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
Professional Activities
-
PC:
NSDI'19,
SoCC'19,
ENTROPY'19,
SecDev'19,
CoqPL'19,
PLDI'18 ERC,
SecDev'18,
ICFP'18 SRC.
Teaching
- COMS 4115 Programming Languages and Translators (Spring 2019).
- COMS E6998 Formal Verification of System Software (Fall 2018).
- COMS W3101 Programming Languages (Spring 2018).
Selected Awards
- Dec. 2018, Columbia-IBM Center Seed Grant Award, Columbia University.
- Dec. 2016, Distinction Dissertation, Yale University.
- Aug. 2016, Nomination for ACM Dissertation Award, Yale University.
- Feb. 2016, Robert Willets Carle Scholarship, Yale University.
- Aug. 2011, Doctoral Fellowship, Yale University.
- Jul. 2011, Outstanding Undergraduate (67 among 3540), Tsinghua University.
- Jul. 2011, Outstanding Student of Beijing City, China.
- Jul. 2011, Hornors Undergraduate Thesis Award (5 among 140), Tsinghua University.
- Oct. 2010, Sohu Scholarship, Tsinghua University.
- Oct. 2009, Ticket Master Scholarship, Tsinghua University.
- Oct. 2006, First Prize of National Mathematical Olympiad Competition, China.
Office
515 CSB, Columbia University
Phone
+1 (212) 939-7111
CertiKOS Layers (for fun)
