Ronghui Gu

Hiring!

My Columbia lab is looking for Ph.D. students and Postdocs. Check out our recent OSDI'21 (Best Paper Award), 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

August 2021	VRM is accepted to appear at SOSP 2021.
July 2021	Awarded Amazon Research Awards (co-PI).
July 2021	DistAI won the Jay Lepreau Best Paper Award at OSDI 2021.
June 2021	Became a member of Sigma Xi.
June 2021	Selected as The Top 100 Yale Alumni In Technology Of 2021.
May 2021	Grant on Verifying Software on Arm Hardware is funded by NSF.
April 2021	Grant on Verified Enclave Layers ($4,563,980) is funded by DARPA.
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.

Education

• Ph.D. in Computer Science, Yale University, December 2016
• 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).

Select Publications

• [SOSP 2021] Verifying a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware.
  R. Tao, J. Yao, Shih-Wei Li, X. Li, J. Nieh, and R. Gu

• [USENIX Security 2021] Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor.
  S. Li, X. Li, R. Gu, J. Nieh, and J. Hui

• [OSDI 2021] DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols.
  J. Yao, R. Tao, R. Gu, J. Nieh, S. Jana, and G. Ryan.
  OSDI Jay Lepreau Best Paper Award

• [PLDI 2021] 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] A Secure and Formally Verified Linux KVM Hypervisor.
  S. Li, X. Li, R. Gu, J. Nieh, and J. Hui
  Media coverage: Columbia Engineering News

• [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 (co-PI), July 2021.

Jay Lepreau Award, July 2021.

Member, Sigma Xi, June 2021.

The Top 100 Yale Alumni In Technology Of 2021, June 2021.

Amazon Research Awards, April 2021.

Named the inaugural Tang Family Assistant Professor, Janurary 2021.

Columbia University’s Final Nominee for the Packard Fellowship, March 2020.

SOSP Best Paper Award, October 2019.

Communications of the ACM (CACM) Research Highlights, October 2019.

MIT Technology Review 35 Innovators Under 35 Semi-Finalist, Feburary 2019.

Distinguished Dissertation Award, Yale University, December 2016.

Yale Nominee, ACM Doctoral Dissertation Award, August 2016.

Robert Willets Carle Scholarship, Yale University, Feburary 2016.

Graduation with Highest Distinction (3 out of 140), Tsinghua University, July 2011.

Outstanding Undergraduate of Beijing City, China, July 2011.

Honors Undergraduate Thesis Award (5 out of 140), Tsinghua University, July 2011.

Program Committees

ASPLOS 2022 ERC	PLDI 2022	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 2021).
• 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.