Ronghui Gu

Registered user since Fri 22 Jan 2016

Name:Ronghui Gu

Ronghui Gu is the inaugural Tang Family Assistant Professor of Computer Science at Columbia University. His thesis work on building certified OS kernels received the Yale Doctoral Dissertation Award and was nominated for the ACM Doctoral Dissertation Award. He is the primary designer and developer of CertiKOS, the first verified concurrent OS kernel, and SeKVM, the first verified commodity cloud hypervisor–major milestones toward building safe and secure systems software. Gu also founded CertiK, a Web3 cybersecurity unicorn startup valued at $1 billion and backed by Tiger Global, Sequoia, and Coatue. CertiK has collectively served more than 1,800 enterprise clients and secured more than $300 billion worth of assets in cryptocurrency. For his work in systems verification, Gu received: an OSDI Jay Lepreau Best Paper Award, two Amazon Research Awards, an SOSP Best Paper Award, and a CACM Research Highlight. He obtained his Ph.D. degree from Yale University in 2016 and bachelor’s degree from Tsinghua University in 2011.

Country:United States
Affiliation:Columbia University
Research interests:Programming Languages, Operating Systems, and Blockchain, with a focus on systems verification and proof automation.


PLDI 2023 Author of Gleipnir: toward practical error analysis for Quantum programs within the PLDI Research Papers-track
PLDI 2022 Author of Giallar: Push-button Verification for the Qiskit Quantum Compiler within the PLDI-track
Committee Member in PLDI within the PLDI-track
POPL 2022 Committee Member in Program Committee within the POPL-track
PLDI 2021 Author of Gleipnir: Toward Practical Error Analysis for Quantum Programs within the PLDI-track
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