Ronghui Gu is a tenure-track Assistant Professor of Computer Science at Columbia University. He obtained his Ph.D. in Computer Science from Yale University in 2016, where his dissertation won Yale's Distinction Dissertation Award and was nominated for the ACM Dissertation Award. He obtained his B.S. from Tsinghua University in 2011. Ronghui is an expert in formal verification of system software. He was the primary designer and developer of CertiKOS, the world's first fully verified concurrent OS kernel. His OSDI16 paper on CertiKOS has been nominated and selected for publication in the Research Highlights section of the CACM.