Ronghui Gu

Hiring!

My research group at Columbia University is looking for Ph.D./Master students, and Postdocs. Check out our recent 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 bug-free and hacker-resistant systems software.

Education

• Aug. 2011 to Aug. 2016, Yale University, Ph.D. in Computer Science.
• 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, Graduation with Highest Distinction (top 1.9%)

Manuscripts

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

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

Select Awards

Columbia University’s Final Nominee for the Packard Fellowship	Mar. 2020
SOSP Best Paper Award	Oct. 2019
Communications of the ACM (CACM) Research Highlights	Oct. 2019
MIT Technology Review 35 Innovators Under 35 Semi-Finalist	Feb. 2019
Distinction Dissertation, Yale University	Dec. 2016
Yale Nominee, ACM Doctoral Dissertation Award	Aug. 2016
Robert Willets Carle Scholarship, Yale University	Feb. 2016
Graduation with Highest Distinction (top 1.9%), Tsinghua University	July 2011
Outstanding Undergraduate of Beijing City, China	July 2011
Honors Undergraduate Thesis Award (5 among 140), Tsinghua University	July 2011

Program Committees

OSDI 2021	PLDI 2020	SecDev 2020	NSDI 2019	SoCC 2019
CoqPL 2019	SecDev 2019	PLDI 2018 ERC	SecDev 2018	ICFP 2018 SRC

Students

• PhD: Runzhou Tao, John Zhuang Hui, Jianan Yao, Xupeng Li, Maxwell Levatich, and Xuheng Li.
• BS: Justin Wong, River Dillon Keefer, Jerry Lin.
• Student collaborators: Shih-wei Li, Yunong Shi (UChicago), Gabriel Ryan, Mengqi Liu (Yale), and Xinhao Yuan.

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.