Ronghui Gu

Registered user since Fri 22 Jan 2016

Name: Ronghui Gu

Bio: Ronghui Gu is an Assistant Professor of Computer Science at Columbia University. He got his Ph.D. from Yale University in 2016 on the verification of system software, for which he received the Yale Distinction Dissertation Award and was nominated for the ACM Dissertation Award. Gu’s research centers on certified software systems software and spans many fields ranging from programming language design, OS kernel development, formal semantics, compiler development, proof engineering, to concurrency and distributed computing. In recent years, as the primary designer and developer, he and his colleagues at Yale developed the formally verified concurrent OS kernel CertiKOS—a major milestone toward building safe and secure software systems. Gu also co-founded CertiK, a formal verification startup focusing on building trustworthy smart contracts and blockchain ecosystems.

Affiliation: Columbia University, USA

Personal website:

Research interests: Programming languages and operating systems, with a focus on language-based support for safety and security, certified system software, certified programming and compilation, formal methods, and concurrency.


PLDI 2020 Committee Member in Program Committee within the PLDI Research Papers-track
Author of Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks within the PLDI Research Papers-track
POPL 2020 Author of Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation within the Research Papers-track
ICFP 2018 Committee Member in Selection Committee within the Student Research Competition-track
PLDI 2018 Committee Member in External Review Committee
Author of Certified Concurrent Abstraction Layers within the PLDI Research Papers-track
PLDI 2016 Author of Toward Compositional Verification of Interruptible OS Kernels and Device Drivers within the Research Papers-track
Author of End-to-End Verification of Information-Flow Security for C and Assembly Programs within the Research Papers-track