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.
• Aug. 2007 to Jul. 2011, Tsinghua University, B.S. in Computer Science.

Selected Publications

• [SOSP 2019][New] Serval: Scaling Symbolic Evaluation for Automated Verification of Systems Code.

  L. Nelson, J. Bornholt, R. Gu, A. Baumann, E. Torlak, X. Wang

• [SOSP 2019][New] Using Concurrent Relational Logic with Helper for Verifying the AtomFS File System.

  M. Zou, H. Ding, D. Du, M. Fu, R. Gu, H. Chen

• [CACM][New] 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

Program Committee

PLDI'20, NSDI'19, SoCC'19, SecDev'19, CoqPL'19, PLDI'18 ERC, SecDev'18 ICFP'18 SRC.

Teaching

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

Selected Awards

• Feb. 2019, MIT Technology Review 35 Innovators Under 35 Semi-Finalist.
• 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.