Ronghui Gu (顾荣辉)

Hiring!

My research group at Columbia University is looking for Ph.D./Master students, and Postdocs. 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
• Yale Nominee of the ACM Doctoral 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 Publications

• [CACM] Building Certified Concurrent OS Kernels.

  R. Gu, Z. Shao, H. Chen, J. Kim, J. Koenig, X. Wu, V. Sjoberg, and D. Constanzo.

  Honor: selected in the Research Highlights section.

• [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

• [CAV 2018] Partial Order Aware Concurrency Sampling.

  X. Yuan, J. Yang, and R. Gu

• [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, 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

Professional Activities

Program Committee:
PLDI'20, 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).
• Graduate Seminar on Systems.

Selected Awards

• Dec. 2018, Columbia-IBM Center Seed Grant Award, Columbia University.
• Dec. 2016, Distinction Dissertation, Yale University.
• Aug. 2016, Yale Nominee, ACM Doctoral Dissertation Award.
• 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.